Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 18:06 4ff9b82a

View on Github →

feat(data/set/lattice): new lemma Union_singleton_eq_range (#10819)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.range_id'

Modified src/data/set/intervals/proj_Icc.lean

Modified src/data/set/lattice.lean

modified theorem set.Union_of_singleton

modified theorem set.Union_of_singleton_coe

added theorem set.Union_singleton_eq_range

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/integral/lebesgue.lean