Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-04 10:47 78fe862a

View on Github →

chore(measure_theory/lebesgue_measure): review (#3686)

  • use ennreal.of_real instead of coe ∘ nnreal.of_real;
  • avoid some non-finishing simps;
  • 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.

Estimated changes

added theorem ennreal.of_real_add_le
modified theorem ennreal.to_real_of_real
modified theorem real.volume_Icc
modified theorem real.volume_Ico
added theorem real.volume_Ioc
modified theorem real.volume_Ioo
modified theorem real.volume_singleton