File tree Expand file tree Collapse file tree
MeasureTheory/Measure/Lebesgue Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -88,10 +88,6 @@ theorem volume_real_Ico_of_le {a b : ℝ} (hab : a ≤ b) : volume.real (Ico a b
8888@[simp]
8989theorem volume_Icc {a b : ℝ} : volume (Icc a b) = ofReal (b - a) := by simp [volume_val]
9090
91- @[simp]
92- theorem volume_uIcc {a b : ℝ} : volume (uIcc a b) = ofReal |b - a| := by
93- simp [uIcc, volume_Icc, max_sub_min_eq_abs]
94-
9591@[simp]
9692theorem volume_real_Icc {a b : ℝ} : volume.real (Icc a b) = max (b - a) 0 := by
9793 simp [measureReal_def, ENNReal.toReal_ofReal']
Original file line number Diff line number Diff line change @@ -377,7 +377,7 @@ lemma uIoo_subset_Ioo (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂
377377@[simp] lemma nonempty_uIoo [DenselyOrdered α] : (uIoo a b).Nonempty ↔ a ≠ b := by
378378 simp [uIoo, eq_comm]
379379
380- @[simp] lemma nonempty_uIoc [DenselyOrdered α] : (uIoc a b).Nonempty ↔ a ≠ b := by
380+ @[simp] lemma nonempty_uIoc : (uIoc a b).Nonempty ↔ a ≠ b := by
381381 simp [uIoc, eq_comm]
382382
383383lemma uIoo_eq_union : uIoo a b = Ioo a b ∪ Ioo b a := by
You can’t perform that action at this time.
0 commit comments