Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-18 23:42 c3e40bef

View on Github →

feat(data/equiv/local_equiv): define piecewise and disjoint_union (#6700) Also change some lemmas to use set.ite.

Estimated changes

Modified src/data/equiv/local_equiv.lean

added def local_equiv.disjoint_union

added theorem local_equiv.is_image.apply_mem_iff

added theorem local_equiv.is_image.iff_preimage_eq

added theorem local_equiv.is_image.iff_symm_preimage_eq

added theorem local_equiv.is_image.image_eq

added theorem local_equiv.is_image.left_inv_on_piecewise

added theorem local_equiv.is_image.of_image_eq

added theorem local_equiv.is_image.of_symm_image_eq

added def local_equiv.is_image.restr

added theorem local_equiv.is_image.symm_apply_mem_iff

added theorem local_equiv.is_image.symm_iff

added theorem local_equiv.is_image.symm_image_eq

added theorem local_equiv.is_image.symm_maps_to

added def local_equiv.is_image

added theorem local_equiv.is_image_source_target

added def local_equiv.piecewise

added def local_equiv.simps.inv_fun

added theorem local_equiv.symm_piecewise

Modified src/data/indicator_function.lean

Modified src/data/set/basic.lean

added theorem set.ite_empty_left

added theorem set.ite_empty_right

Modified src/data/set/function.lean

added theorem set.eq_on.piecewise_ite'

added theorem set.eq_on.piecewise_ite

added theorem set.eq_on_piecewise

added theorem set.maps_to.piecewise_ite

Modified src/measure_theory/integration.lean

Modified src/measure_theory/measurable_space.lean

added theorem measurable_set.ite

Modified src/measure_theory/set_integral.lean