Equiv

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

Statistics

Metric	Count
Definitions `toUniformEquivOfIsUniformInducing`, `UniformEquiv`, `apply`, `symm_apply`, `changeInv`, `finTwoArrow`, `funUnique`, `image`, `instEquivLike`, `ofIsUniformEmbedding`, `piCongr`, `piCongrLeft`, `piCongrRight`, `piFinTwo`, `prodAssoc`, `prodComm`, `prodCongr`, `prodPUnit`, `prodPunit`, `punitProd`, `refl`, `setCongr`, `subtype`, `toEquiv`, `toHomeomorph`, `trans`, `ulift`, `«term_≃ᵤ_»`	28
Theorems `apply_symm_apply`, `bijective`, `coe_prodComm`, `coe_prodCongr`, `coe_punitProd`, `coe_symm_toEquiv`, `coe_toEquiv`, `comap_eq`, `completeSpace_iff`, `continuous`, `continuous_symm`, `ext`, `ext_iff`, `finTwoArrow_apply`, `finTwoArrow_symm_apply`, `funUnique_apply`, `funUnique_symm_apply`, `image_preimage`, `image_symm`, `injective`, `isUniformEmbedding`, `isUniformInducing`, `piCongrLeft_apply`, `piCongrLeft_apply_apply`, `piCongrLeft_refl`, `piCongrLeft_symm_apply`, `piCongrLeft_toEquiv`, `piCongrRight_apply`, `piCongrRight_refl`, `piCongrRight_symm`, `piCongrRight_toEquiv`, `piCongr_apply`, `piCongr_toEquiv`, `piFinTwo_apply`, `piFinTwo_symm_apply`, `preimage_image`, `preimage_symm`, `prodComm_symm`, `prodCongr_symm`, `prodPUnit_apply`, `range_coe`, `refl_apply`, `refl_symm`, `self_comp_symm`, `subtype_apply_coe`, `subtype_symm_apply_coe`, `surjective`, `symm_apply_apply`, `symm_comp_self`, `toEquiv_injective`, `toHomeomorph_apply`, `toHomeomorph_symm_apply`, `trans_apply`, `uniformContinuous`, `uniformContinuous_invFun`, `uniformContinuous_symm`, `uniformContinuous_toFun`, `uniformEquiv_mk_coe`, `uniformEquiv_mk_coe_symm`	59
Total	87

Equiv

Definitions

Name	Category	Theorems
`toUniformEquivOfIsUniformInducing` 📖	CompOp	—

UniformEquiv

Definitions

Name	Category	Theorems
`changeInv` 📖	CompOp	—
`finTwoArrow` 📖	CompOp	2 math math: `finTwoArrow_apply`, `finTwoArrow_symm_apply`
`funUnique` 📖	CompOp	2 math math: `funUnique_apply`, `funUnique_symm_apply`
`image` 📖	CompOp	—
`instEquivLike` 📖	CompOp	55 math math: `funUnique_apply`, `refl_apply`, `AbstractCompletion.mapEquiv_coe`, `Padic.withValUniformEquiv_norm_le_one_iff`, `self_comp_symm`, `Valuation.IsEquiv.valuedCompletion_le_one_iff`, `coe_toEquiv`, `continuous_symm`, `trans_apply`, `uniformContinuous_symm`, `AbstractCompletion.uniformContinuous_compareEquiv`, `UniformSpace.Completion.mapEquiv_coe`, `image_preimage`, `piCongrLeft_symm_apply`, `coe_prodComm`, `apply_symm_apply`, `coe_symm_toEquiv`, `finTwoArrow_apply`, `symm_comp_self`, `image_symm`, `finTwoArrow_symm_apply`, `comap_eq`, `Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv`, `injective`, `continuous`, `funUnique_symm_apply`, `uniformContinuous`, `preimage_symm`, `ext_iff`, `prodPUnit_apply`, `Padic.withValUniformEquiv_cast_apply`, `isUniformInducing`, `range_coe`, `Metric.Snowflaking.uniformEquiv_symm_apply`, `uniformEquiv_mk_coe`, `coe_punitProd`, `symm_apply_apply`, `bijective`, `coe_prodCongr`, `CompareReals.compare_uc_symm`, `isUniformEmbedding`, `Metric.Snowflaking.uniformEquiv_apply`, `piCongr_apply`, `uniformEquiv_mk_coe_symm`, `toHomeomorph_symm_apply`, `piCongrLeft_apply_apply`, `toHomeomorph_apply`, `CompareReals.compare_uc`, `surjective`, `piFinTwo_symm_apply`, `piCongrLeft_apply`, `piFinTwo_apply`, `preimage_image`, `AbstractCompletion.uniformContinuous_compareEquiv_symm`, `piCongrRight_apply`
`ofIsUniformEmbedding` 📖	CompOp	—
`piCongr` 📖	CompOp	2 math math: `piCongr_toEquiv`, `piCongr_apply`
`piCongrLeft` 📖	CompOp	5 math math: `piCongrLeft_refl`, `piCongrLeft_symm_apply`, `piCongrLeft_toEquiv`, `piCongrLeft_apply_apply`, `piCongrLeft_apply`
`piCongrRight` 📖	CompOp	4 math math: `piCongrRight_refl`, `piCongrRight_symm`, `piCongrRight_toEquiv`, `piCongrRight_apply`
`piFinTwo` 📖	CompOp	2 math math: `piFinTwo_symm_apply`, `piFinTwo_apply`
`prodAssoc` 📖	CompOp	—
`prodComm` 📖	CompOp	2 math math: `coe_prodComm`, `prodComm_symm`
`prodCongr` 📖	CompOp	2 math math: `prodCongr_symm`, `coe_prodCongr`
`prodPUnit` 📖	CompOp	1 math math: `prodPUnit_apply`
`prodPunit` 📖	CompOp	—
`punitProd` 📖	CompOp	1 math math: `coe_punitProd`
`refl` 📖	CompOp	4 math math: `refl_apply`, `piCongrLeft_refl`, `refl_symm`, `piCongrRight_refl`
`setCongr` 📖	CompOp	—
`subtype` 📖	CompOp	2 math math: `subtype_apply_coe`, `subtype_symm_apply_coe`
`toEquiv` 📖	CompOp	13 math math: `WithLp.toEquiv_uniformEquivProd`, `PiLp.toEquiv_uniformEquiv`, `coe_toEquiv`, `Metric.Snowflaking.uniformEquiv_toEquiv`, `coe_symm_toEquiv`, `toEquiv_injective`, `piCongrLeft_toEquiv`, `uniformContinuous_toFun`, `piCongr_toEquiv`, `LaurentSeries.comparePkg_eq_extension`, `piCongr_apply`, `piCongrRight_toEquiv`, `uniformContinuous_invFun`
`toHomeomorph` 📖	CompOp	4 math math: `PiLp.toHomeomorph_uniformEquiv`, `WithLp.toHomeomorph_uniformEquivProd`, `toHomeomorph_symm_apply`, `toHomeomorph_apply`
`trans` 📖	CompOp	1 math math: `trans_apply`
`ulift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.bijective`
`coe_prodComm` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `instUniformSpaceProd` `EquivLike.toFunLike` `instEquivLike` `prodComm`	—	—
`coe_prodCongr` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `instUniformSpaceProd` `EquivLike.toFunLike` `instEquivLike` `prodCongr`	—	—
`coe_punitProd` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `instUniformSpaceProd` `instUniformSpacePUnit` `EquivLike.toFunLike` `instEquivLike` `punitProd`	—	—
`coe_symm_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `UniformEquiv` `instEquivLike` `symm`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `UniformEquiv` `instEquivLike`	—	—
`comap_eq` 📖	mathematical	—	`UniformSpace.comap` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`IsUniformInducing.comap_uniformSpace` `isUniformInducing`
`completeSpace_iff` 📖	mathematical	—	`CompleteSpace`	—	`completeSpace_congr` `isUniformEmbedding`
`continuous` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`UniformContinuous.continuous` `uniformContinuous`
`continuous_symm` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`UniformContinuous.continuous` `uniformContinuous_symm`
`ext` 📖	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`toEquiv_injective` `Equiv.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`finTwoArrow_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `instUniformSpaceProd` `EquivLike.toFunLike` `instEquivLike` `finTwoArrow`	—	—
`finTwoArrow_symm_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `instUniformSpaceProd` `Pi.uniformSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `finTwoArrow` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `EquivLike.toFunLike` `instEquivLike` `funUnique` `Unique.instInhabited`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `funUnique` `uniqueElim`	—	—
`image_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.preimage`	—	`Equiv.image_preimage`
`image_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.preimage`	—	`Equiv.image_eq_preimage_symm`
`injective` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.injective`
`isUniformEmbedding` 📖	mathematical	—	`IsUniformEmbedding` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`isUniformInducing` `injective`
`isUniformInducing` 📖	mathematical	—	`IsUniformInducing` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`IsUniformInducing.of_comp` `uniformContinuous` `symm_comp_self`
`piCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft` `Equiv.symm` `Equiv.piCongrLeft'`	—	—
`piCongrLeft_apply_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft`	—	`Equiv.piCongrLeft_apply_apply`
`piCongrLeft_refl` 📖	mathematical	—	`piCongrLeft` `Equiv.refl` `refl` `Pi.uniformSpace`	—	—
`piCongrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `symm` `piCongrLeft`	—	—
`piCongrLeft_toEquiv` 📖	mathematical	—	`toEquiv` `Pi.uniformSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `piCongrLeft` `Equiv.piCongrLeft`	—	—
`piCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `EquivLike.toFunLike` `instEquivLike` `piCongrRight`	—	—
`piCongrRight_refl` 📖	mathematical	—	`piCongrRight` `refl` `Pi.uniformSpace`	—	—
`piCongrRight_symm` 📖	mathematical	—	`symm` `Pi.uniformSpace` `piCongrRight`	—	—
`piCongrRight_toEquiv` 📖	mathematical	—	`toEquiv` `Pi.uniformSpace` `piCongrRight` `Equiv.piCongrRight`	—	—
`piCongr_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `EquivLike.toFunLike` `instEquivLike` `piCongr` `Equiv` `Equiv.instEquivLike` `Equiv.piCongrLeft` `Equiv.piCongrRight` `toEquiv`	—	—
`piCongr_toEquiv` 📖	mathematical	—	`toEquiv` `Pi.uniformSpace` `piCongr` `Equiv.trans` `Equiv.piCongrRight` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piCongrLeft`	—	—
`piFinTwo_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `Pi.uniformSpace` `instUniformSpaceProd` `EquivLike.toFunLike` `instEquivLike` `piFinTwo`	—	—
`piFinTwo_symm_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `instUniformSpaceProd` `Pi.uniformSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `piFinTwo` `Fin.cons` `finZeroElim`	—	—
`preimage_image` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.image`	—	`Equiv.preimage_image`
`preimage_symm` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.image`	—	`Equiv.image_eq_preimage_symm`
`prodComm_symm` 📖	mathematical	—	`symm` `instUniformSpaceProd` `prodComm`	—	—
`prodCongr_symm` 📖	mathematical	—	`symm` `instUniformSpaceProd` `prodCongr`	—	—
`prodPUnit_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `instUniformSpaceProd` `instUniformSpacePUnit` `EquivLike.toFunLike` `instEquivLike` `prodPUnit`	—	—
`range_coe` 📖	mathematical	—	`Set.range` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.univ`	—	`EquivLike.range_eq_univ`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`apply_symm_apply`
`subtype_apply_coe` 📖	mathematical	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	`instUniformSpaceSubtype` `subtype`	—	—
`subtype_symm_apply_coe` 📖	mathematical	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	`instUniformSpaceSubtype` `symm` `subtype`	—	—
`surjective` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`symm_apply_apply`
`toEquiv_injective` 📖	mathematical	—	`UniformEquiv` `Equiv` `toEquiv`	—	—
`toHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorph` `UniformEquiv` `instEquivLike`	—	—
`toHomeomorph_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorph` `UniformEquiv` `instEquivLike` `symm`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`uniformContinuous` 📖	mathematical	—	`UniformContinuous` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`uniformContinuous_toFun`
`uniformContinuous_invFun` 📖	mathematical	—	`UniformContinuous` `Equiv.invFun` `toEquiv`	—	—
`uniformContinuous_symm` 📖	mathematical	—	`UniformContinuous` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`uniformContinuous_invFun`
`uniformContinuous_toFun` 📖	mathematical	—	`UniformContinuous` `Equiv.toFun` `toEquiv`	—	—
`uniformEquiv_mk_coe` 📖	mathematical	`UniformContinuous` `Equiv.toFun` `Equiv.invFun`	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike`	—	—
`uniformEquiv_mk_coe_symm` 📖	mathematical	`UniformContinuous` `Equiv.toFun` `Equiv.invFun`	`DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	—

UniformEquiv.Simps

Definitions

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

(root)

Definitions

Name	Category	Theorems
`UniformEquiv` 📖	CompData	56 math math: `UniformEquiv.funUnique_apply`, `UniformEquiv.refl_apply`, `AbstractCompletion.mapEquiv_coe`, `Padic.withValUniformEquiv_norm_le_one_iff`, `UniformEquiv.self_comp_symm`, `Valuation.IsEquiv.valuedCompletion_le_one_iff`, `UniformEquiv.coe_toEquiv`, `UniformEquiv.continuous_symm`, `UniformEquiv.trans_apply`, `UniformEquiv.uniformContinuous_symm`, `AbstractCompletion.uniformContinuous_compareEquiv`, `UniformSpace.Completion.mapEquiv_coe`, `UniformEquiv.image_preimage`, `UniformEquiv.piCongrLeft_symm_apply`, `UniformEquiv.coe_prodComm`, `UniformEquiv.apply_symm_apply`, `UniformEquiv.coe_symm_toEquiv`, `UniformEquiv.finTwoArrow_apply`, `UniformEquiv.symm_comp_self`, `UniformEquiv.image_symm`, `UniformEquiv.finTwoArrow_symm_apply`, `UniformEquiv.toEquiv_injective`, `UniformEquiv.comap_eq`, `Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv`, `UniformEquiv.injective`, `UniformEquiv.continuous`, `UniformEquiv.funUnique_symm_apply`, `UniformEquiv.uniformContinuous`, `UniformEquiv.preimage_symm`, `UniformEquiv.ext_iff`, `UniformEquiv.prodPUnit_apply`, `Padic.withValUniformEquiv_cast_apply`, `UniformEquiv.isUniformInducing`, `UniformEquiv.range_coe`, `Metric.Snowflaking.uniformEquiv_symm_apply`, `UniformEquiv.uniformEquiv_mk_coe`, `UniformEquiv.coe_punitProd`, `UniformEquiv.symm_apply_apply`, `UniformEquiv.bijective`, `UniformEquiv.coe_prodCongr`, `CompareReals.compare_uc_symm`, `UniformEquiv.isUniformEmbedding`, `Metric.Snowflaking.uniformEquiv_apply`, `UniformEquiv.piCongr_apply`, `UniformEquiv.uniformEquiv_mk_coe_symm`, `UniformEquiv.toHomeomorph_symm_apply`, `UniformEquiv.piCongrLeft_apply_apply`, `UniformEquiv.toHomeomorph_apply`, `CompareReals.compare_uc`, `UniformEquiv.surjective`, `UniformEquiv.piFinTwo_symm_apply`, `UniformEquiv.piCongrLeft_apply`, `UniformEquiv.piFinTwo_apply`, `UniformEquiv.preimage_image`, `AbstractCompletion.uniformContinuous_compareEquiv_symm`, `UniformEquiv.piCongrRight_apply`
`«term_≃ᵤ_»` 📖	CompOp	—

---

← Back to Index