ContinuousAffineEquiv

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

Statistics

Metric	Count
Definitions `ContinuousAffineEquiv`, `apply`, `symm_apply`, `constVAdd`, `instEquivLike`, `instFunLike`, `prodAssoc`, `prodComm`, `prodCongr`, `refl`, `toAffineEquiv`, `toContinuousAffineMap`, `toHomeomorph`, `trans`, `toContinuousAffineEquiv`, `«term_≃ᴬ[_]_»`	16
Theorems `apply_eq_iff_eq`, `apply_eq_iff_eq_symm_apply`, `apply_symm_apply`, `bijective`, `coe_coe`, `coe_refl`, `coe_symm_toAffineEquiv`, `coe_symm_toEquiv`, `coe_toContinuousAffineMap`, `coe_toEquiv`, `coe_trans`, `constVAdd_coe`, `continuous`, `continuous_invFun`, `continuous_toFun`, `eq_symm_apply`, `ext`, `ext_iff`, `image_eq_preimage_symm`, `image_preimage`, `image_symm`, `image_symm_eq_preimage`, `image_symm_image`, `injective`, `instHomeomorphClass`, `preimage_image`, `preimage_symm`, `prodAssoc_apply`, `prodAssoc_symm_apply`, `prodAssoc_toAffineEquiv`, `prodComm_apply`, `prodComm_symm`, `prodComm_symm_apply`, `prodComm_toAffineEquiv`, `prodCongr_apply`, `prodCongr_symm`, `prodCongr_toAffineEquiv`, `prodCongr_toContinuousAffineMap`, `refl_apply`, `refl_symm`, `refl_trans`, `self_trans_symm`, `surjective`, `symm_apply_apply`, `symm_apply_eq`, `symm_bijective`, `symm_image_image`, `symm_refl`, `symm_symm`, `symm_symm_apply`, `symm_trans_self`, `toAffineEquiv_injective`, `toAffineEquiv_refl`, `toAffineEquiv_symm`, `toContinuousAffineMap_injective`, `toContinuousAffineMap_toAffineMap`, `toContinuousAffineMap_toContinuousMap`, `toEquiv_refl`, `toEquiv_symm`, `trans_apply`, `trans_assoc`, `trans_refl`, `trans_toContinuousAffineMap`, `coe_toContinuousAffineEquiv`, `toContinuousAffineEquiv_toContinuousAffineMap`	65
Total	81

ContinuousAffineEquiv

Definitions

Name	Category	Theorems
`constVAdd` 📖	CompOp	1 math math: `constVAdd_coe`
`instEquivLike` 📖	CompOp	1 math math: `instHomeomorphClass`
`instFunLike` 📖	CompOp	39 math math: `image_symm_eq_preimage`, `prodComm_apply`, `injective`, `symm_symm_apply`, `coe_toContinuousAffineMap`, `AmpleSet.preimage_iff`, `symm_apply_apply`, `image_preimage`, `prodCongr_apply`, `ContinuousLinearEquiv.coe_toContinuousAffineEquiv`, `refl_apply`, `symm_apply_eq`, `preimage_symm`, `coe_toEquiv`, `apply_symm_apply`, `apply_eq_iff_eq`, `apply_eq_iff_eq_symm_apply`, `AmpleSet.preimage`, `ext_iff`, `trans_apply`, `coe_refl`, `surjective`, `coe_trans`, `AmpleSet.image_iff`, `continuous`, `coe_symm_toEquiv`, `image_eq_preimage_symm`, `preimage_image`, `AffineIsometryEquiv.coe_symm_toContinuousAffineEquiv`, `bijective`, `prodAssoc_apply`, `coe_symm_toAffineEquiv`, `coe_coe`, `image_symm`, `AmpleSet.image`, `symm_image_image`, `image_symm_image`, `eq_symm_apply`, `AffineIsometryEquiv.coe_toContinuousAffineEquiv`
`prodAssoc` 📖	CompOp	3 math math: `prodAssoc_toAffineEquiv`, `prodAssoc_apply`, `prodAssoc_symm_apply`
`prodComm` 📖	CompOp	4 math math: `prodComm_apply`, `prodComm_symm_apply`, `prodComm_toAffineEquiv`, `prodComm_symm`
`prodCongr` 📖	CompOp	4 math math: `prodCongr_toContinuousAffineMap`, `prodCongr_apply`, `prodCongr_symm`, `prodCongr_toAffineEquiv`
`refl` 📖	CompOp	11 math math: `symm_trans_self`, `self_trans_symm`, `refl_apply`, `AffineIsometryEquiv.toContinuousAffineEquiv_refl`, `trans_refl`, `refl_trans`, `coe_refl`, `toEquiv_refl`, `refl_symm`, `symm_refl`, `toAffineEquiv_refl`
`toAffineEquiv` 📖	CompOp	18 math math: `prodAssoc_toAffineEquiv`, `toEquiv_symm`, `prodComm_symm_apply`, `coe_toEquiv`, `prodComm_toAffineEquiv`, `constVAdd_coe`, `toAffineEquiv_injective`, `toEquiv_refl`, `coe_symm_toEquiv`, `continuous_toFun`, `continuous_invFun`, `toAffineEquiv_symm`, `coe_symm_toAffineEquiv`, `prodCongr_toAffineEquiv`, `coe_coe`, `toContinuousAffineMap_toAffineMap`, `prodAssoc_symm_apply`, `toAffineEquiv_refl`
`toContinuousAffineMap` 📖	CompOp	7 math math: `coe_toContinuousAffineMap`, `prodCongr_toContinuousAffineMap`, `ContinuousLinearEquiv.toContinuousAffineEquiv_toContinuousAffineMap`, `trans_toContinuousAffineMap`, `toContinuousAffineMap_injective`, `toContinuousAffineMap_toContinuousMap`, `toContinuousAffineMap_toAffineMap`
`toHomeomorph` 📖	CompOp	1 math math: `toContinuousAffineMap_toContinuousMap`
`trans` 📖	CompOp	8 math math: `symm_trans_self`, `self_trans_symm`, `trans_toContinuousAffineMap`, `trans_refl`, `trans_apply`, `refl_trans`, `coe_trans`, `trans_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	`Equiv.apply_eq_iff_eq`
`apply_eq_iff_eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`Equiv.apply_symm_apply`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	`Equiv.bijective`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `AffineEquiv.equivLike` `toAffineEquiv` `ContinuousAffineEquiv` `instFunLike`	—	—
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `refl`	—	—
`coe_symm_toAffineEquiv` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.symm` `toAffineEquiv` `ContinuousAffineEquiv` `instFunLike` `symm`	—	—
`coe_symm_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `AffineEquiv.toEquiv` `toAffineEquiv` `ContinuousAffineEquiv` `instFunLike` `symm`	—	—
`coe_toContinuousAffineMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `ContinuousAffineMap.instFunLike` `toContinuousAffineMap` `ContinuousAffineEquiv` `instFunLike`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `AffineEquiv.toEquiv` `toAffineEquiv` `ContinuousAffineEquiv` `instFunLike`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `trans`	—	—
`constVAdd_coe` 📖	mathematical	—	`toAffineEquiv` `constVAdd` `AffineEquiv.constVAdd`	—	—
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	`continuous_toFun`
`continuous_invFun` 📖	mathematical	—	`Continuous` `Equiv.invFun` `AffineEquiv.toEquiv` `toAffineEquiv`	—	—
`continuous_toFun` 📖	mathematical	—	`Continuous` `Equiv.toFun` `AffineEquiv.toEquiv` `toAffineEquiv`	—	—
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`Equiv.eq_symm_apply`
`ext` 📖	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	`ext`
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `Set.preimage` `symm`	—	`Equiv.image_eq_preimage_symm`
`image_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `Set.preimage`	—	`Function.Surjective.image_preimage` `surjective`
`image_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm` `Set.preimage`	—	`Equiv.image_eq_preimage_symm`
`image_symm_eq_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm` `Set.preimage`	—	`image_eq_preimage_symm` `symm_symm`
`image_symm_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`symm_image_image`
`injective` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	`Equiv.injective`
`instHomeomorphClass` 📖	mathematical	—	`HomeomorphClass` `ContinuousAffineEquiv` `instEquivLike`	—	`continuous_toFun` `continuous_invFun`
`preimage_image` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `Set.image`	—	`Function.Injective.preimage_image` `injective`
`preimage_symm` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm` `Set.image`	—	`image_symm`
`prodAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `Prod.instAddGroup` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `instFunLike` `prodAssoc`	—	—
`prodAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `Prod.instAddGroup` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.symm` `toAffineEquiv` `instTopologicalSpaceProd` `prodAssoc`	—	—
`prodAssoc_toAffineEquiv` 📖	mathematical	—	`toAffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `Prod.instAddGroup` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `prodAssoc` `AffineEquiv.prodAssoc`	—	—
`prodComm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `instFunLike` `prodComm`	—	—
`prodComm_symm` 📖	mathematical	—	`symm` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `prodComm`	—	—
`prodComm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.symm` `toAffineEquiv` `instTopologicalSpaceProd` `prodComm`	—	—
`prodComm_toAffineEquiv` 📖	mathematical	—	`toAffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `prodComm` `AffineEquiv.prodComm`	—	—
`prodCongr_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `instFunLike` `prodCongr`	—	—
`prodCongr_symm` 📖	mathematical	—	`symm` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `prodCongr`	—	—
`prodCongr_toAffineEquiv` 📖	mathematical	—	`toAffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `prodCongr` `AffineEquiv.prodCongr`	—	—
`prodCongr_toContinuousAffineMap` 📖	mathematical	—	`toContinuousAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instTopologicalSpaceProd` `prodCongr` `ContinuousAffineMap.prodMap`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `refl`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	`ext`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_apply_apply`
`surjective` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `ContinuousAffineEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_image_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	`Equiv.symm_image_image`
`symm_refl` 📖	mathematical	—	`symm` `refl`	—	—
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `symm`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `apply_symm_apply`
`toAffineEquiv_injective` 📖	mathematical	—	`ContinuousAffineEquiv` `AffineEquiv` `toAffineEquiv`	—	—
`toAffineEquiv_refl` 📖	mathematical	—	`toAffineEquiv` `refl` `AffineEquiv.refl`	—	—
`toAffineEquiv_symm` 📖	mathematical	—	`toAffineEquiv` `symm` `AffineEquiv.symm`	—	—
`toContinuousAffineMap_injective` 📖	mathematical	—	`ContinuousAffineEquiv` `ContinuousAffineMap` `toContinuousAffineMap`	—	`ext`
`toContinuousAffineMap_toAffineMap` 📖	mathematical	—	`ContinuousAffineMap.toAffineMap` `toContinuousAffineMap` `AffineEquiv.toAffineMap` `toAffineEquiv`	—	—
`toContinuousAffineMap_toContinuousMap` 📖	mathematical	—	`ContinuousAffineMap.toContinuousMap` `toContinuousAffineMap` `toContinuousMap` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `HomeomorphClass.instContinuousMapClass` `HomeomorphClass.instHomeomorph` `toHomeomorph`	—	—
`toEquiv_refl` 📖	mathematical	—	`AffineEquiv.toEquiv` `toAffineEquiv` `refl` `Equiv.refl`	—	—
`toEquiv_symm` 📖	mathematical	—	`AffineEquiv.toEquiv` `toAffineEquiv` `symm` `Equiv.symm`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `instFunLike` `trans`	—	—
`trans_assoc` 📖	mathematical	—	`trans`	—	`ext`
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	`ext`
`trans_toContinuousAffineMap` 📖	mathematical	—	`toContinuousAffineMap` `trans` `ContinuousAffineMap.comp`	—	—

ContinuousAffineEquiv.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`toContinuousAffineEquiv` 📖	CompOp	2 math math: `coe_toContinuousAffineEquiv`, `toContinuousAffineEquiv_toContinuousAffineMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toContinuousAffineEquiv` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineEquiv.instFunLike` `toContinuousAffineEquiv` `ContinuousLinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids`
`toContinuousAffineEquiv_toContinuousAffineMap` 📖	mathematical	—	`ContinuousAffineEquiv.toContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `toContinuousAffineEquiv` `ContinuousLinearMap.toContinuousAffineMap` `toContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids`

(root)

Definitions

Name	Category	Theorems
`ContinuousAffineEquiv` 📖	CompData	44 math math: `ContinuousAffineEquiv.image_symm_eq_preimage`, `ContinuousAffineEquiv.prodComm_apply`, `ContinuousAffineEquiv.injective`, `ContinuousAffineEquiv.instHomeomorphClass`, `ContinuousAffineEquiv.symm_symm_apply`, `ContinuousAffineEquiv.coe_toContinuousAffineMap`, `AmpleSet.preimage_iff`, `ContinuousAffineEquiv.symm_apply_apply`, `ContinuousAffineEquiv.image_preimage`, `ContinuousAffineEquiv.prodCongr_apply`, `ContinuousLinearEquiv.coe_toContinuousAffineEquiv`, `ContinuousAffineEquiv.refl_apply`, `ContinuousAffineEquiv.symm_apply_eq`, `ContinuousAffineEquiv.preimage_symm`, `ContinuousAffineEquiv.coe_toEquiv`, `ContinuousAffineEquiv.apply_symm_apply`, `ContinuousAffineEquiv.apply_eq_iff_eq`, `ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply`, `AmpleSet.preimage`, `ContinuousAffineEquiv.ext_iff`, `ContinuousAffineEquiv.trans_apply`, `ContinuousAffineEquiv.toAffineEquiv_injective`, `ContinuousAffineEquiv.coe_refl`, `ContinuousAffineEquiv.surjective`, `ContinuousAffineEquiv.coe_trans`, `AmpleSet.image_iff`, `ContinuousAffineEquiv.continuous`, `ContinuousAffineEquiv.coe_symm_toEquiv`, `ContinuousAffineEquiv.image_eq_preimage_symm`, `ContinuousAffineEquiv.preimage_image`, `ContinuousAffineEquiv.toContinuousAffineMap_injective`, `AffineIsometryEquiv.coe_symm_toContinuousAffineEquiv`, `ContinuousAffineEquiv.bijective`, `ContinuousAffineEquiv.prodAssoc_apply`, `ContinuousAffineEquiv.coe_symm_toAffineEquiv`, `ContinuousAffineEquiv.coe_coe`, `AffineIsometryEquiv.toContinuousAffineEquiv_injective`, `ContinuousAffineEquiv.image_symm`, `AmpleSet.image`, `ContinuousAffineEquiv.symm_bijective`, `ContinuousAffineEquiv.symm_image_image`, `ContinuousAffineEquiv.image_symm_image`, `ContinuousAffineEquiv.eq_symm_apply`, `AffineIsometryEquiv.coe_toContinuousAffineEquiv`
`«term_≃ᴬ[_]_»` 📖	CompOp	—

---

← Back to Index