Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 13:06 7d331eb9

View on Github →

chore(*): assorted lemmas about set and finset (#3158)

Estimated changes

Modified src/data/finset.lean

added theorem finset.bUnion_coe

added theorem finset.bUnion_preimage_singleton

Modified src/data/indicator_function.lean

added theorem set.eq_on_indicator

added theorem set.indicator_preimage_of_not_mem

added theorem set.mem_range_indicator

Modified src/data/set/basic.lean

added theorem set.preimage_const

added theorem set.preimage_const_of_mem

added theorem set.preimage_const_of_not_mem

modified theorem set.preimage_inter_range

added theorem set.preimage_range

added theorem set.preimage_range_inter

added theorem set.preimage_singleton_eq_empty

added theorem set.preimage_singleton_nonempty

added theorem set.sep_mem_eq

Modified src/data/set/disjointed.lean

added theorem pairwise_disjoint_fiber

added theorem set.pairwise_on_univ

Modified src/data/set/lattice.lean

added theorem set.bUnion_preimage_singleton

added theorem set.bUnion_range_preimage_singleton

added theorem set.pairwise_on_disjoint_fiber

Modified src/logic/basic.lean

added theorem ite_eq_iff

Modified src/measure_theory/integration.lean