Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-31 08:47 10ebb718

View on Github →

feat(measure_theory): induction principles in measure theory (#3978) This commit adds three induction principles for measure theory

  • To prove something for arbitrary simple functions
  • To prove something for arbitrary measurable functions into ennreal
  • To prove something for arbitrary measurable + integrable functions. This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs.

Estimated changes

added theorem pi.comp_one
added theorem pi.const_one
added theorem pi.one_comp
added theorem set.comp_indicator
modified theorem set.indicator_comp_of_zero
added theorem set.indicator_zero'
modified theorem ennreal.div_pos_iff
modified theorem ennreal.div_zero_iff
modified theorem ennreal.mul_eq_top
modified theorem ennreal.mul_lt_top
modified theorem ennreal.mul_ne_top
modified theorem ennreal.mul_pos
added theorem ennreal.not_lt_top
modified theorem ennreal.to_real_eq_to_real
modified theorem ennreal.to_real_mul_to_real
added theorem eq.subset
added theorem set.diff_diff_comm
modified theorem set.image_compl_preimage
added theorem set.comp_piecewise
added theorem set.piecewise_same
added theorem set.range_piecewise
added theorem function.comp_const
added theorem function.const_apply
added theorem function.const_comp
modified theorem function.injective.of_comp
modified theorem function.left_inverse.comp
modified theorem function.right_inverse.comp
modified theorem function.surjective.of_comp