Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-21 21:22 ca1b2d1d

View on Github →

refactor(analysis/measure_theory/measurable_space): derive complete lattice structure from Galois insertion

Estimated changes

Modified analysis/measure_theory/measurable_space.lean

added theorem measurable_space.generate_from_le_iff

added def measurable_space.gi_generate_from

added theorem measurable_space.is_measurable_bot_iff

added theorem measurable_space.is_measurable_top

added theorem measurable_space.mk_of_closure_sets

Modified analysis/measure_theory/measure_space.lean

Modified analysis/topology/continuity.lean