Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-11 21:55 bf58bf44

View on Github →

feat(topology/measurable_space): induction rule for sigma-algebras with intersection-stable generators; uses Dynkin systems

Estimated changes

Modified topology/measurable_space.lean

added theorem is_measurable_univ

added theorem measurable_generate_from

added theorem measurable_space.dynkin_system.dynkin_system_eq

added def measurable_space.dynkin_system.generate

added theorem measurable_space.dynkin_system.generate_from_eq

added inductive measurable_space.dynkin_system.generate_has

added theorem measurable_space.dynkin_system.generate_inter

added theorem measurable_space.dynkin_system.generate_le

added theorem measurable_space.dynkin_system.has_sdiff

added theorem measurable_space.dynkin_system.has_union

added theorem measurable_space.dynkin_system.has_univ

added def measurable_space.dynkin_system.of_measurable_space

added theorem measurable_space.dynkin_system.of_measurable_space_le_of_measurable_space_iff

added theorem measurable_space.dynkin_system.of_measurable_space_to_measurable_space

added def measurable_space.dynkin_system.restrict_on

added def measurable_space.dynkin_system.to_measurable_space

added structure measurable_space.dynkin_system

added def measurable_space.generate_from

added theorem measurable_space.generate_from_le

added inductive measurable_space.generate_measurable

added theorem measurable_space.induction_on_inter

added theorem measurable_space.is_measurable_generate_from

added theorem nat.lt_succ_iff

added theorem set.disjoint_disjointed

added def set.disjointed

added theorem set.disjointed_Union