Commit 2020-08-03 19:22 40c6a295

View on Github →

feat(measure_theory/content): define outer measure from content (#3649) Part of the development for the Haar measure: define an outer measure from a content.

Estimated changes

Created src/measure_theory/content.lean

added def measure_theory.inner_content

added theorem measure_theory.inner_content_Sup_nat

added theorem measure_theory.inner_content_Union_nat

added theorem measure_theory.inner_content_empty

added theorem measure_theory.inner_content_exists_compact

added theorem measure_theory.inner_content_le

added theorem measure_theory.inner_content_mono'

added theorem measure_theory.inner_content_mono

added theorem measure_theory.inner_content_of_is_compact

added theorem measure_theory.inner_content_pos

added theorem measure_theory.is_left_invariant_inner_content

added theorem measure_theory.le_inner_content

added theorem measure_theory.outer_measure.le_of_content_compacts

added def measure_theory.outer_measure.of_content

added theorem measure_theory.outer_measure.of_content_exists_compact

added theorem measure_theory.outer_measure.of_content_exists_open

added theorem measure_theory.outer_measure.of_content_interior_compacts

added theorem measure_theory.outer_measure.of_content_opens

added theorem measure_theory.outer_measure.of_content_pos_of_is_open