mathlib3
78fe862a - chore(measure_theory/lebesgue_measure): review (#3686)

Commit
5 years ago
chore(measure_theory/lebesgue_measure): review (#3686) * use `ennreal.of_real` instead of `coe ∘ nnreal.of_real`; * avoid some non-finishing `simp`s; * simplify proofs of `lebesgue_outer_Ico/Ioc/Ioo`; * add `instance : locally_finite_measure (volume : measure ℝ)` instead of `real.volume_lt_top_of_bounded` and `real.volume_lt_top_of_compact`.
Author
Parents
Loading