Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 16:22 8713c0bd

View on Github →

feat(measure/pi): prove extensionality for measure.pi (#6304)

  • If two measures in a finitary product are equal on cubes with measurable sides (or with sides in a set generating the corresponding sigma-algebra), then the measures are equal.
  • Add sigma_finite instance for measure.pi
  • Some basic lemmas about sets (more specifically Union and set.pi)
  • rename measurable_set.pi_univ -> measurable_set.univ_pi (pi univ t is called univ_pi consistently in set/basic, but it's not always consistent elsewhere)
  • rename [bs]?Union_prod -> [bs]?Union_prod_const

Estimated changes

added theorem nat.surjective_unpair
added theorem set.eval_preimage'
added theorem set.eval_preimage
added theorem set.univ_pi_ite
added theorem set.Inter_congr
added theorem set.Union_congr
modified theorem set.Union_of_singleton
modified theorem set.Union_prod
added theorem set.Union_prod_const
modified theorem set.Union_subset_Union2
added theorem set.Union_univ_pi
deleted theorem set.bUnion_prod
added theorem set.bUnion_prod_const
modified theorem set.directed_on_Union
modified theorem set.preimage_Union
deleted theorem set.sUnion_prod
added theorem set.sUnion_prod_const
added theorem set.univ_pi_eq_Inter
deleted theorem measurable_set.pi_univ
added theorem measurable_set.univ_pi
added theorem generate_from_eq_pi
added theorem generate_from_pi
added theorem generate_from_pi_eq
added theorem is_pi_system.pi
added theorem is_pi_system_pi