Commit 2025-01-02 11:03 6f76ae27

View on Github →

feat(Topology/Group): continuous isomorphism (#16991) Define the continuous isomorphisms of multiplicative and additive topological group.

Estimated changes

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added structure ContinuousAddEquiv

added theorem ContinuousMulEquiv.apply_eq_iff_eq

added theorem ContinuousMulEquiv.apply_eq_iff_symm_apply

added theorem ContinuousMulEquiv.apply_symm_apply

added theorem ContinuousMulEquiv.coe_mk'

added theorem ContinuousMulEquiv.coe_mk

added theorem ContinuousMulEquiv.coe_refl

added theorem ContinuousMulEquiv.coe_toHomeomorph_symm

added theorem ContinuousMulEquiv.coe_trans

added theorem ContinuousMulEquiv.comp_symm_eq

added theorem ContinuousMulEquiv.eq_comp_symm

added theorem ContinuousMulEquiv.eq_symm_apply

added theorem ContinuousMulEquiv.eq_symm_comp

added theorem ContinuousMulEquiv.equivLike_inv_eq_symm

added theorem ContinuousMulEquiv.ext

added theorem ContinuousMulEquiv.invFun_eq_symm

added def ContinuousMulEquiv.mk'

added def ContinuousMulEquiv.ofUnique

added def ContinuousMulEquiv.refl

added theorem ContinuousMulEquiv.refl_apply

added theorem ContinuousMulEquiv.self_comp_symm

added theorem ContinuousMulEquiv.self_trans_symm

added def ContinuousMulEquiv.symm

added theorem ContinuousMulEquiv.symm_apply_apply

added theorem ContinuousMulEquiv.symm_apply_eq

added theorem ContinuousMulEquiv.symm_comp_eq

added theorem ContinuousMulEquiv.symm_comp_self

added theorem ContinuousMulEquiv.symm_symm

added theorem ContinuousMulEquiv.symm_trans_apply

added theorem ContinuousMulEquiv.symm_trans_self

added theorem ContinuousMulEquiv.toEquiv_eq_coe

added theorem ContinuousMulEquiv.toHomeomorph_eq_coe

added theorem ContinuousMulEquiv.toMulEquiv_eq_coe

added def ContinuousMulEquiv.trans

added theorem ContinuousMulEquiv.trans_apply

added structure ContinuousMulEquiv