Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-20 03:17 cd884eb8

View on Github →

feat(measure_theory): finite_spanning_sets_in (#4668)

  • We define a new Type-valued structure finite_spanning_sets_in which consists of a countable sequence of sets that span the type, have finite measure, and live in a specified collection of sets,
  • sigma_finite is redefined in terms of finite_spanning_sets_in
  • One of the ext lemmas is now conveniently formulated in terms of finite_spanning_sets_in
  • finite_spanning_sets_in is also used to remove a little bit of code duplication in prod (which occurred because sigma_finite was a Prop, and forgot the actual construction)
  • Define a predicate is_countably_spanning which states that a collection of sets has a countable spanning subset. This is useful for one particular lemma in prod.
  • Generalize some lemmas about products in the case that the σ-algebras are generated by a collection of sets. This can be used to reason about iterated products.
  • Prove prod_assoc_prod.
  • Cleanup in measurable_space and somewhat in measure_space.
  • Rename measurable.sum_rec -> measurable.sum_elim (and give a different but definitionally equal statement)

Estimated changes

added theorem set.Union_unpair_prod
added theorem set.Union_prod
added theorem set.bUnion_prod
added theorem set.prod_Union
added theorem set.prod_bUnion
added theorem set.prod_sUnion
added theorem set.sUnion_prod
modified theorem is_measurable.Inter
modified theorem is_measurable.Inter_Prop
modified theorem is_measurable.Union
modified theorem is_measurable.Union_Prop
modified theorem is_measurable.disjointed
modified theorem is_measurable.sInter
modified theorem is_measurable.sUnion
modified theorem is_measurable.subtype_image
modified theorem measurable.comp
modified theorem measurable.fst
modified theorem measurable.indicator
modified theorem measurable.piecewise
modified theorem measurable.snd
modified theorem measurable.subtype_coe
modified theorem measurable.subtype_mk
added theorem measurable.sum_elim
deleted theorem measurable.sum_rec
modified theorem measurable_const
modified theorem measurable_equiv.coe_eq
modified def measurable_equiv.symm
modified theorem measurable_find
modified theorem measurable_find_greatest'
modified theorem measurable_find_greatest
modified theorem measurable_from_nat
modified theorem measurable_from_top
modified theorem measurable_id
modified theorem measurable_one
modified theorem measurable_pi_apply
modified theorem measurable_pi_lambda
modified theorem measurable_space.comap_bot
modified theorem measurable_space.comap_supr
modified theorem measurable_space.ext
modified theorem measurable_space.map_top
modified structure measurable_space
modified theorem measurable_subtype_coe
modified theorem measurable_to_encodable
modified theorem measurable_to_nat
modified theorem measurable_unit
modified theorem subsingleton.measurable
modified def completion
modified def null_measurable
added theorem generate_from_eq_prod
added theorem generate_from_prod_eq
added theorem is_pi_system.prod