Commit 2024-01-29 17:52 7afbac66

View on Github →

chore(Topology/PartialHomeomorph): rename type variables (#9632) Greek letters are dead, long live X, Y and Z. Same procedure as in previous renames.

Estimated changes

Modified Mathlib/Topology/PartialHomeomorph.lean

modified def Homeomorph.toPartialHomeomorph

modified def Homeomorph.toPartialHomeomorphOfImageEq

modified def Homeomorph.transPartialHomeomorph

modified theorem Homeomorph.transPartialHomeomorph_eq_trans

modified theorem Homeomorph.transPartialHomeomorph_trans

modified theorem Homeomorph.trans_transPartialHomeomorph

modified theorem OpenEmbedding.toPartialHomeomorph_left_inv

modified theorem OpenEmbedding.toPartialHomeomorph_right_inv

modified theorem PartialHomeomorph.EqOnSource.eqOn

modified theorem PartialHomeomorph.EqOnSource.restr

modified theorem PartialHomeomorph.EqOnSource.source_eq

modified theorem PartialHomeomorph.EqOnSource.symm'

modified theorem PartialHomeomorph.EqOnSource.symm_eqOn_target

modified theorem PartialHomeomorph.EqOnSource.target_eq

modified theorem PartialHomeomorph.EqOnSource.trans'

modified def PartialHomeomorph.EqOnSource

modified theorem PartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn

modified theorem PartialHomeomorph.IsImage.leftInvOn_piecewise

modified def PartialHomeomorph.IsImage.restr

modified theorem PartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn

modified def PartialHomeomorph.IsImage

modified theorem PartialHomeomorph.Set.EqOn.restr_eqOn_source

modified def PartialHomeomorph.Simps.apply

modified def PartialHomeomorph.Simps.symm_apply

modified theorem PartialHomeomorph.coe_coe

modified theorem PartialHomeomorph.coe_coe_symm

modified theorem PartialHomeomorph.coe_trans

modified theorem PartialHomeomorph.coe_trans_symm

modified theorem PartialHomeomorph.continuousAt_iff_continuousAt_comp_left

modified theorem PartialHomeomorph.continuousAt_iff_continuousAt_comp_right

modified theorem PartialHomeomorph.continuousAt_symm

modified theorem PartialHomeomorph.continuousOn_iff_continuousOn_comp_left

modified theorem PartialHomeomorph.continuousOn_iff_continuousOn_comp_right

modified theorem PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left

modified theorem PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right

modified theorem PartialHomeomorph.continuous_iff_continuous_comp_left

modified def PartialHomeomorph.disjointUnion

modified theorem PartialHomeomorph.eqOnSource_iff

modified theorem PartialHomeomorph.eq_of_eqOnSource_univ

modified theorem PartialHomeomorph.eq_of_partialEquiv_eq

modified theorem PartialHomeomorph.eq_symm_apply

modified theorem PartialHomeomorph.eventually_nhds'

modified theorem PartialHomeomorph.eventually_nhds

modified theorem PartialHomeomorph.eventually_nhdsWithin'

modified theorem PartialHomeomorph.eventually_nhdsWithin

modified def PartialHomeomorph.homeomorphOfImageSubsetSource

modified theorem PartialHomeomorph.image_eq_target_inter_inv_preimage

modified theorem PartialHomeomorph.image_mem_nhds

modified theorem PartialHomeomorph.image_source_inter_eq'

modified theorem PartialHomeomorph.image_source_inter_eq

modified theorem PartialHomeomorph.invFun_eq_coe

modified theorem PartialHomeomorph.isImage_source_target_of_disjoint

modified theorem PartialHomeomorph.isOpen_image_iff_of_subset_source

modified theorem PartialHomeomorph.isOpen_image_of_subset_source

modified theorem PartialHomeomorph.isOpen_image_source_inter

modified theorem PartialHomeomorph.isOpen_image_symm_of_subset_target

modified theorem PartialHomeomorph.isOpen_inter_preimage

modified theorem PartialHomeomorph.isOpen_inter_preimage_symm

modified theorem PartialHomeomorph.isOpen_symm_image_iff_of_subset_target

modified theorem PartialHomeomorph.left_inv

modified theorem PartialHomeomorph.map_nhdsWithin_eq

modified theorem PartialHomeomorph.map_nhdsWithin_preimage_eq

modified theorem PartialHomeomorph.map_source

modified theorem PartialHomeomorph.map_subtype_source

modified theorem PartialHomeomorph.map_target

modified theorem PartialHomeomorph.mk_coe

modified theorem PartialHomeomorph.mk_coe_symm

modified theorem PartialHomeomorph.nhdsWithin_source_inter

modified theorem PartialHomeomorph.nhdsWithin_target_inter

modified def PartialHomeomorph.ofContinuousOpen

modified def PartialHomeomorph.ofContinuousOpenRestrict

modified def PartialHomeomorph.ofSet

modified theorem PartialHomeomorph.ofSet_trans'

modified theorem PartialHomeomorph.ofSet_trans

modified theorem PartialHomeomorph.ofSet_trans_ofSet

modified theorem PartialHomeomorph.ofSet_univ_eq_refl

modified def PartialHomeomorph.pi

modified def PartialHomeomorph.piecewise

modified theorem PartialHomeomorph.preimage_closure

modified theorem PartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter

modified theorem PartialHomeomorph.preimage_frontier

modified theorem PartialHomeomorph.preimage_interior

modified def PartialHomeomorph.prod

modified theorem PartialHomeomorph.prod_eq_prod_of_nonempty'

modified theorem PartialHomeomorph.prod_eq_prod_of_nonempty

modified theorem PartialHomeomorph.prod_symm

modified theorem PartialHomeomorph.prod_trans

modified theorem PartialHomeomorph.refl_partialEquiv

modified theorem PartialHomeomorph.refl_prod_refl

modified theorem PartialHomeomorph.refl_symm

modified theorem PartialHomeomorph.refl_trans

modified def PartialHomeomorph.replaceEquiv

modified theorem PartialHomeomorph.replaceEquiv_eq_self

modified theorem PartialHomeomorph.restrOpen_source

modified theorem PartialHomeomorph.restrOpen_toPartialEquiv

modified theorem PartialHomeomorph.restr_eq_of_source_subset

modified theorem PartialHomeomorph.restr_source'

modified theorem PartialHomeomorph.restr_source_inter

modified theorem PartialHomeomorph.restr_toPartialEquiv'

modified theorem PartialHomeomorph.restr_toPartialEquiv

modified theorem PartialHomeomorph.restr_trans

modified theorem PartialHomeomorph.restr_univ

modified theorem PartialHomeomorph.right_inv

modified theorem PartialHomeomorph.secondCountableTopology_source

modified theorem PartialHomeomorph.source_inter_preimage_inv_preimage

modified theorem PartialHomeomorph.source_inter_preimage_target_inter

modified theorem PartialHomeomorph.subtypeRestr_symm_eqOn

modified theorem PartialHomeomorph.subtypeRestr_symm_eqOn_of_le

modified theorem PartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr

modified theorem PartialHomeomorph.symm_image_eq_source_inter_preimage

modified theorem PartialHomeomorph.symm_image_target_inter_eq

modified theorem PartialHomeomorph.symm_piecewise

modified theorem PartialHomeomorph.target_inter_inv_preimage_preimage

modified def PartialHomeomorph.toFun'

modified theorem PartialHomeomorph.toFun_eq_coe

modified def PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv

modified def PartialHomeomorph.transHomeomorph

modified theorem PartialHomeomorph.transHomeomorph_eq_trans

modified theorem PartialHomeomorph.transHomeomorph_transHomeomorph

modified theorem PartialHomeomorph.trans_apply

modified theorem PartialHomeomorph.trans_assoc

modified theorem PartialHomeomorph.trans_ofSet

modified theorem PartialHomeomorph.trans_of_set'

modified theorem PartialHomeomorph.trans_refl

modified theorem PartialHomeomorph.trans_transHomeomorph

modified structure PartialHomeomorph

modified theorem TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_coe