Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-15 14:04 1444fa52

View on Github →

fix(haar_measure): minor changes (#4623) There were some mistakes in the doc, which made it sound like chaar and haar_outer_measure coincide on compact sets, which is not generally true. Also cleanup various proofs.

Estimated changes

Modified src/measure_theory/content.lean

added theorem measure_theory.outer_measure.of_content_le

Modified src/measure_theory/haar_measure.lean

deleted theorem measure_theory.measure.chaar_le_haar_outer_measure

added theorem measure_theory.measure.echaar_le_haar_outer_measure

added theorem measure_theory.measure.haar.echaar_self

modified theorem measure_theory.measure.haar.is_left_invariant_chaar

added theorem measure_theory.measure.haar.is_left_invariant_echaar

modified theorem measure_theory.measure.haar.is_left_invariant_index

deleted theorem measure_theory.measure.haar_outer_measure_le_chaar

added theorem measure_theory.measure.haar_outer_measure_le_echaar