Commit 2021-03-29 23:43 ad4aca0c

View on Github →

feat(topology/local_homeomorph): add is_image, piecewise, and disjoint_union (#6804) Also add local_equiv.copy and local_homeomorph.replace_equiv and use them for local_equiv.disjoint_union and `local_homeomorph.disjoint_union.

Estimated changes

Modified src/data/equiv/local_equiv.lean

added def local_equiv.copy

added theorem local_equiv.copy_eq_self

added theorem local_equiv.disjoint_union_eq_piecewise

added theorem local_equiv.is_image.inter_eq_of_inter_eq_of_eq_on

added theorem local_equiv.is_image.symm_eq_on_of_inter_eq_of_eq_on

added theorem local_equiv.is_image_source_target_of_disjoint

Modified src/data/set/basic.lean

modified theorem set.diff_union_self

added theorem set.ite_inter_of_inter_eq

added theorem set.ite_left

added theorem set.ite_right

added theorem set.preimage_ite

added theorem set.subset_ite

modified theorem set.union_diff_self

Modified src/data/set/function.lean

added theorem set.eq_on_empty

modified theorem set.piecewise_eq_of_mem

modified theorem set.piecewise_eq_of_not_mem

Modified src/geometry/manifold/charted_space.lean

Modified src/topology/basic.lean

added theorem frontier_subset_closure

added theorem is_open.inter_frontier_eq

added theorem is_open.inter_frontier_eq_empty_of_disjoint

Modified src/topology/continuous_on.lean

added theorem continuous_on_piecewise_ite'

added theorem continuous_on_piecewise_ite

added theorem ite_inter_closure_compl_eq_of_inter_frontier_eq

added theorem ite_inter_closure_eq_of_inter_frontier_eq

Modified src/topology/local_homeomorph.lean

added def local_homeomorph.disjoint_union

modified theorem local_homeomorph.image_mem_nhds

added theorem local_homeomorph.is_image.apply_mem_iff

added theorem local_homeomorph.is_image.iff_preimage_eq'

added theorem local_homeomorph.is_image.iff_preimage_eq

added theorem local_homeomorph.is_image.iff_symm_preimage_eq'

added theorem local_homeomorph.is_image.iff_symm_preimage_eq

added theorem local_homeomorph.is_image.image_eq

added theorem local_homeomorph.is_image.inter_eq_of_inter_eq_of_eq_on

added theorem local_homeomorph.is_image.is_open_iff

added theorem local_homeomorph.is_image.left_inv_on_piecewise

added theorem local_homeomorph.is_image.map_nhds_within_eq

added theorem local_homeomorph.is_image.of_image_eq

added theorem local_homeomorph.is_image.of_symm_image_eq

added def local_homeomorph.is_image.restr

added theorem local_homeomorph.is_image.symm_apply_mem_iff

added theorem local_homeomorph.is_image.symm_eq_on_of_inter_eq_of_eq_on

added theorem local_homeomorph.is_image.symm_iff

added theorem local_homeomorph.is_image.symm_image_eq

added theorem local_homeomorph.is_image.symm_maps_to

added theorem local_homeomorph.is_image.to_local_equiv

added def local_homeomorph.is_image

added theorem local_homeomorph.is_image_source_target

added theorem local_homeomorph.is_image_source_target_of_disjoint

modified theorem local_homeomorph.map_nhds_eq

added def local_homeomorph.piecewise

added theorem local_homeomorph.piecewise_coe

added theorem local_homeomorph.piecewise_to_local_equiv

modified theorem local_homeomorph.preimage_open_of_open_symm

modified theorem local_homeomorph.prod_to_local_equiv

added def local_homeomorph.replace_equiv

added theorem local_homeomorph.replace_equiv_eq_self

modified theorem local_homeomorph.source_preimage_target

modified theorem local_homeomorph.symm_map_nhds_eq

added theorem local_homeomorph.symm_piecewise

modified theorem local_homeomorph.tendsto_symm