Equiv

📁 Source: Mathlib/Topology/Algebra/Algebra/Equiv.lean

Statistics

Metric	Count
Definitions `cast`, `equivLike`, `instCoeContinuousLinearEquivId`, `refl`, `toAlgEquiv`, `toContinuousAlgHom`, `toContinuousLinearEquiv`, `toHomeomorph`, `trans`, `ContinuousAlgEquivClass`, `«term_≃A[_]_»`	11
Theorems `isUniformEmbedding`, `apply_symm_apply`, `cast_apply`, `cast_symm_apply`, `coe_apply`, `coe_coe`, `coe_comp_coe_symm`, `coe_inj`, `coe_injective`, `coe_mk`, `coe_refl`, `coe_refl'`, `coe_symm_comp_coe`, `coe_toAlgEquiv`, `comp_coe`, `comp_continuous_iff`, `comp_continuous_iff'`, `continuous`, `continuousAlgEquivClass`, `continuousAt`, `continuousOn`, `continuousWithinAt`, `continuous_invFun`, `continuous_toFun`, `eq_symm_apply`, `ext`, `ext_iff`, `image_closure`, `image_eq_preimage_symm`, `image_symm_eq_preimage`, `image_symm_image`, `isClosed_image`, `isOpenMap`, `isUniformEmbedding`, `map_eq_zero_iff`, `map_nhds_eq`, `preimage_closure`, `preimage_symm_preimage`, `refl_apply`, `refl_symm`, `refl_toContinuousLinearEquiv`, `self_comp_symm`, `surjective`, `symm_apply_apply`, `symm_apply_eq`, `symm_bijective`, `symm_comp_self`, `symm_image_image`, `symm_map_nhds_eq`, `symm_preimage_preimage`, `symm_symm`, `symm_symm_apply`, `symm_toAlgEquiv`, `symm_toHomeomorph`, `symm_trans_apply`, `toAlgEquiv_injective`, `toContinuousLinearEquiv_apply`, `toContinuousLinearEquiv_symm`, `toContinuousLinearEquiv_toLinearEquiv_eq`, `toContinuousLinearMap_toContinuousLinearEquiv_eq`, `trans_apply`, `trans_toAlgEquiv`, `trans_toContinuousLinearEquiv`, `toAlgEquivClass`, `toHomeomorphClass`	65
Total	76

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniformEmbedding` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `AlgEquiv` `Ring.toSemiring` `instFunLike` `symm`	`IsUniformEmbedding`	—	`ContinuousAlgEquiv.isUniformEmbedding`

ContinuousAlgEquiv

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	2 math math: `cast_symm_apply`, `cast_apply`
`equivLike` 📖	CompOp	50 math math: `map_nhds_eq`, `symm_apply_eq`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `continuousOn`, `ContinuousLinearEquiv.conjContinuousAlgEquiv_apply`, `continuous`, `symm_trans_apply`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `symm_map_nhds_eq`, `toContinuousLinearEquiv_apply`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `ext_iff`, `continuousWithinAt`, `isOpenMap`, `comp_continuous_iff`, `image_closure`, `cast_symm_apply`, `isClosed_image`, `symm_comp_self`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `image_eq_preimage_symm`, `coe_toAlgEquiv`, `trans_apply`, `symm_symm_apply`, `symm_apply_apply`, `symm_image_image`, `eq_symm_apply`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `refl_apply`, `continuousAlgEquivClass`, `image_symm_eq_preimage`, `self_comp_symm`, `map_eq_zero_iff`, `comp_coe`, `coe_coe`, `preimage_symm_preimage`, `cast_apply`, `surjective`, `comp_continuous_iff'`, `apply_symm_apply`, `preimage_closure`, `coe_apply`, `image_symm_image`, `continuousAt`, `coe_mk`, `symm_preimage_preimage`, `isUniformEmbedding`, `coe_refl'`, `ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply`, `ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply`
`instCoeContinuousLinearEquivId` 📖	CompOp	—
`refl` 📖	CompOp	6 math math: `ContinuousLinearEquiv.conjContinuousAlgEquiv_refl`, `refl_toContinuousLinearEquiv`, `refl_symm`, `coe_refl`, `refl_apply`, `coe_refl'`
`toAlgEquiv` 📖	CompOp	8 math math: `continuous_invFun`, `trans_toAlgEquiv`, `continuous_toFun`, `coe_toAlgEquiv`, `toAlgEquiv_injective`, `symm_toAlgEquiv`, `toContinuousLinearEquiv_toLinearEquiv_eq`, `comp_coe`
`toContinuousAlgHom` 📖	CompOp	8 math math: `toContinuousLinearMap_toContinuousLinearEquiv_eq`, `coe_inj`, `coe_injective`, `coe_comp_coe_symm`, `coe_refl`, `coe_coe`, `coe_apply`, `coe_symm_comp_coe`
`toContinuousLinearEquiv` 📖	CompOp	6 math math: `toContinuousLinearMap_toContinuousLinearEquiv_eq`, `toContinuousLinearEquiv_symm`, `refl_toContinuousLinearEquiv`, `trans_toContinuousLinearEquiv`, `toContinuousLinearEquiv_apply`, `toContinuousLinearEquiv_toLinearEquiv_eq`
`toHomeomorph` 📖	CompOp	1 math math: `symm_toHomeomorph`
`trans` 📖	CompOp	6 math math: `trans_toAlgEquiv`, `trans_toContinuousLinearEquiv`, `symm_trans_apply`, `ContinuousLinearEquiv.conjContinuousAlgEquiv_trans`, `trans_apply`, `comp_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.right_inv`
`cast_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `cast` `Equiv` `Equiv.instEquivLike` `Equiv.cast`	—	—
`cast_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm` `cast` `Equiv` `Equiv.instEquivLike` `Equiv.cast`	—	—
`coe_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `ContinuousAlgHom.instFunLike` `toContinuousAlgHom` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	—
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `ContinuousAlgHom.instFunLike` `toContinuousAlgHom` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	—
`coe_comp_coe_symm` 📖	mathematical	—	`ContinuousAlgHom.comp` `toContinuousAlgHom` `symm` `ContinuousAlgHom.id`	—	`ContinuousAlgHom.ext` `apply_symm_apply`
`coe_inj` 📖	mathematical	—	`toContinuousAlgHom`	—	`coe_injective`
`coe_injective` 📖	mathematical	—	`ContinuousAlgEquiv` `ContinuousAlgHom` `toContinuousAlgHom`	—	`ext` `ContinuousAlgHom.ext_iff`
`coe_mk` 📖	mathematical	`Continuous` `Equiv.toFun` `AlgEquiv.toEquiv` `Equiv.invFun`	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `AlgEquiv` `AlgEquiv.instFunLike`	—	—
`coe_refl` 📖	mathematical	—	`toContinuousAlgHom` `refl` `ContinuousAlgHom.id`	—	—
`coe_refl'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `refl`	—	—
`coe_symm_comp_coe` 📖	mathematical	—	`ContinuousAlgHom.comp` `toContinuousAlgHom` `symm` `ContinuousAlgHom.id`	—	`ContinuousAlgHom.ext` `symm_apply_apply`
`coe_toAlgEquiv` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `toAlgEquiv` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	—
`comp_coe` 📖	mathematical	—	`AlgHom.comp` `AlgEquiv.toAlgHom` `toAlgEquiv` `AlgHomClass.toAlgHom` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `AlgEquivClass.toAlgHomClass` `ContinuousAlgEquivClass.toAlgEquivClass` `continuousAlgEquivClass` `trans`	—	—
`comp_continuous_iff` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Homeomorph.comp_continuous_iff`
`comp_continuous_iff'` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Homeomorph.comp_continuous_iff'`
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`continuous_toFun`
`continuousAlgEquivClass` 📖	mathematical	—	`ContinuousAlgEquivClass` `ContinuousAlgEquiv` `equivLike`	—	`AlgEquiv.map_mul'` `AlgEquiv.map_add'` `AlgEquiv.commutes'` `continuous_toFun` `continuous_invFun`
`continuousAt` 📖	mathematical	—	`ContinuousAt` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Continuous.continuousAt` `continuous`
`continuousOn` 📖	mathematical	—	`ContinuousOn` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Continuous.continuousOn` `continuous`
`continuousWithinAt` 📖	mathematical	—	`ContinuousWithinAt` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Continuous.continuousWithinAt` `continuous`
`continuous_invFun` 📖	mathematical	—	`Continuous` `Equiv.invFun` `AlgEquiv.toEquiv` `toAlgEquiv`	—	—
`continuous_toFun` 📖	mathematical	—	`Continuous` `Equiv.toFun` `AlgEquiv.toEquiv` `toAlgEquiv`	—	—
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.eq_symm_apply`
`ext` 📖	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	—	`toAlgEquiv_injective` `AlgEquiv.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`ext`
`image_closure` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `closure`	—	`Homeomorph.image_closure`
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `Set.preimage` `symm`	—	`Equiv.image_eq_preimage_symm`
`image_symm_eq_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm` `Set.preimage`	—	`image_eq_preimage_symm` `symm_symm`
`image_symm_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`symm_image_image`
`isClosed_image` 📖	mathematical	—	`IsClosed` `Set.image` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Homeomorph.isClosed_image`
`isOpenMap` 📖	mathematical	—	`IsOpenMap` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`Homeomorph.isOpenMap`
`isUniformEmbedding` 📖	mathematical	—	`IsUniformEmbedding` `DFunLike.coe` `ContinuousAlgEquiv` `Ring.toSemiring` `UniformSpace.toTopologicalSpace` `EquivLike.toFunLike` `equivLike`	—	`Equiv.isUniformEmbedding` `ContinuousAlgHom.uniformContinuous`
`map_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`LinearEquiv.map_eq_zero_iff` `RingHomInvPair.ids`
`map_nhds_eq` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `nhds`	—	`Homeomorph.map_nhds_eq`
`preimage_closure` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `closure`	—	`Homeomorph.preimage_closure`
`preimage_symm_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`symm_preimage_preimage`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `refl`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_toContinuousLinearEquiv` 📖	mathematical	—	`toContinuousLinearEquiv` `refl` `ContinuousLinearEquiv.refl` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	`RingHomInvPair.ids`
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`apply_symm_apply`
`surjective` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike`	—	`AlgEquiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.left_inv`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `ContinuousAlgEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`symm_apply_apply`
`symm_image_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.symm_image_image`
`symm_map_nhds_eq` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm` `nhds`	—	`Homeomorph.symm_map_nhds_eq`
`symm_preimage_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.symm_preimage_preimage`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	—
`symm_toAlgEquiv` 📖	mathematical	—	`toAlgEquiv` `symm` `AlgEquiv.symm`	—	—
`symm_toHomeomorph` 📖	mathematical	—	`toHomeomorph` `symm` `Homeomorph.symm`	—	—
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `symm` `trans`	—	—
`toAlgEquiv_injective` 📖	mathematical	—	`ContinuousAlgEquiv` `AlgEquiv` `toAlgEquiv`	—	—
`toContinuousLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `toContinuousLinearEquiv` `ContinuousAlgEquiv` `equivLike`	—	`RingHomInvPair.ids`
`toContinuousLinearEquiv_symm` 📖	mathematical	—	`toContinuousLinearEquiv` `symm` `ContinuousLinearEquiv.symm` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule`	—	`RingHomInvPair.ids`
`toContinuousLinearEquiv_toLinearEquiv_eq` 📖	mathematical	—	`ContinuousLinearEquiv.toLinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `toContinuousLinearEquiv` `AlgEquiv.toLinearEquiv` `toAlgEquiv`	—	`RingHomInvPair.ids`
`toContinuousLinearMap_toContinuousLinearEquiv_eq` 📖	mathematical	—	`ContinuousLinearEquiv.toContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `toContinuousLinearEquiv` `ContinuousAlgHom.toContinuousLinearMap` `toContinuousAlgHom`	—	`RingHomInvPair.ids`
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgEquiv` `EquivLike.toFunLike` `equivLike` `trans`	—	—
`trans_toAlgEquiv` 📖	mathematical	—	`toAlgEquiv` `trans` `AlgEquiv.trans`	—	—
`trans_toContinuousLinearEquiv` 📖	mathematical	—	`toContinuousLinearEquiv` `trans` `ContinuousLinearEquiv.trans` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule`	—	`RingHomInvPair.ids`

ContinuousAlgEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAlgEquivClass` 📖	mathematical	—	`AlgEquivClass`	—	—
`toHomeomorphClass` 📖	mathematical	—	`HomeomorphClass`	—	—

(root)

Definitions

Name	Category	Theorems
`ContinuousAlgEquivClass` 📖	CompData	1 math math: `ContinuousAlgEquiv.continuousAlgEquivClass`
`«term_≃A[_]_»` 📖	CompOp	—

---

← Back to Index