Commit 2025-01-21 20:44 46d1f440

View on Github →

feat(Topology/Algebra/Algebra/Equiv): continuous algebra equivs (#20609) From FLT. Written by Salvatore Mercuri.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.isUniformEmbedding

added theorem ContinuousAlgEquiv.apply_symm_apply

added theorem ContinuousAlgEquiv.coe_apply

added theorem ContinuousAlgEquiv.coe_coe

added theorem ContinuousAlgEquiv.coe_comp_coe_symm

added theorem ContinuousAlgEquiv.coe_inj

added theorem ContinuousAlgEquiv.coe_injective

added theorem ContinuousAlgEquiv.coe_refl'

added theorem ContinuousAlgEquiv.coe_refl

added theorem ContinuousAlgEquiv.coe_symm_comp_coe

added theorem ContinuousAlgEquiv.coe_toAlgEquiv

added theorem ContinuousAlgEquiv.comp_coe

added theorem ContinuousAlgEquiv.comp_continuous_iff'

added theorem ContinuousAlgEquiv.comp_continuous_iff

added theorem ContinuousAlgEquiv.continuous

added theorem ContinuousAlgEquiv.continuousAt

added theorem ContinuousAlgEquiv.continuousOn

added theorem ContinuousAlgEquiv.continuousWithinAt

added theorem ContinuousAlgEquiv.eq_symm_apply

added theorem ContinuousAlgEquiv.ext

added theorem ContinuousAlgEquiv.image_closure

added theorem ContinuousAlgEquiv.image_eq_preimage

added theorem ContinuousAlgEquiv.image_symm_eq_preimage

added theorem ContinuousAlgEquiv.image_symm_image

added theorem ContinuousAlgEquiv.isClosed_image

added theorem ContinuousAlgEquiv.isOpenMap

added theorem ContinuousAlgEquiv.isUniformEmbedding

added theorem ContinuousAlgEquiv.map_eq_zero_iff

added theorem ContinuousAlgEquiv.map_nhds_eq

added theorem ContinuousAlgEquiv.preimage_closure

added theorem ContinuousAlgEquiv.preimage_symm_preimage

added def ContinuousAlgEquiv.refl

added theorem ContinuousAlgEquiv.refl_apply

added theorem ContinuousAlgEquiv.refl_symm

added theorem ContinuousAlgEquiv.self_comp_symm

added def ContinuousAlgEquiv.symm

added theorem ContinuousAlgEquiv.symm_apply_apply

added theorem ContinuousAlgEquiv.symm_apply_eq

added theorem ContinuousAlgEquiv.symm_comp_self

added theorem ContinuousAlgEquiv.symm_image_image

added theorem ContinuousAlgEquiv.symm_map_nhds_eq

added theorem ContinuousAlgEquiv.symm_preimage_preimage

added theorem ContinuousAlgEquiv.symm_symm

added theorem ContinuousAlgEquiv.symm_symm_apply

added theorem ContinuousAlgEquiv.symm_toAlgEquiv

added theorem ContinuousAlgEquiv.symm_toHomeomorph

added theorem ContinuousAlgEquiv.symm_trans_apply

added theorem ContinuousAlgEquiv.toAlgEquiv_injective

added def ContinuousAlgEquiv.toContinuousAlgHom

added def ContinuousAlgEquiv.trans

added theorem ContinuousAlgEquiv.trans_apply

added theorem ContinuousAlgEquiv.trans_toAlgEquiv

added structure ContinuousAlgEquiv