Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 21:43 3d752421

View on Github →

chore(data/equiv/local_equiv,topology/local_homeomorph): put source/target to the left in ∩ (#6583)

Estimated changes

Modified src/data/equiv/local_equiv.lean

deleted theorem local_equiv.image_inter_source_eq'

deleted theorem local_equiv.image_inter_source_eq

added theorem local_equiv.image_source_inter_eq'

added theorem local_equiv.image_source_inter_eq

deleted theorem local_equiv.symm_image_inter_target_eq'

deleted theorem local_equiv.symm_image_inter_target_eq

added theorem local_equiv.symm_image_target_inter_eq'

added theorem local_equiv.symm_image_target_inter_eq

Modified src/data/set/function.lean

added theorem set.eq_on.inter_preimage_eq

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

Modified src/geometry/manifold/times_cont_mdiff.lean

Modified src/topology/local_homeomorph.lean

modified theorem local_homeomorph.continuous_at_iff_continuous_at_comp_left

deleted theorem local_homeomorph.image_inter_source_eq'

deleted theorem local_homeomorph.image_inter_source_eq

modified theorem local_homeomorph.image_open_of_open'

added theorem local_homeomorph.image_source_inter_eq'

added theorem local_homeomorph.image_source_inter_eq

added theorem local_homeomorph.map_nhds_within_preimage_eq

added theorem local_homeomorph.nhds_within_source_inter

added theorem local_homeomorph.nhds_within_target_inter

added theorem local_homeomorph.source_inter_preimage_inv_preimage

deleted theorem local_homeomorph.symm_image_inter_target_eq

added theorem local_homeomorph.symm_image_target_inter_eq

added theorem local_homeomorph.target_inter_inv_preimage_preimage