DilationEquiv

📁 Source: Mathlib/Topology/MetricSpace/DilationEquiv.lean

Statistics

Metric	Count
Definitions `DilationEquiv`, `symm_apply`, `instEquivLike`, `instGroup`, `ratioHom`, `refl`, `toDilation`, `toEquiv`, `toHomeomorph`, `toPerm`, `trans`, `DilationEquivClass`, `toDilationEquiv`, `«term_≃ᵈ_»`	14
Theorems `apply_symm_apply`, `bijective`, `coe_inv`, `coe_mul`, `coe_one`, `coe_pow`, `coe_symm_toHomeomorph`, `coe_toEquiv`, `coe_toHomeomorph`, `edist_eq'`, `ext`, `ext_iff`, `injective`, `instDilationEquivClass`, `inv_def`, `map_cobounded`, `mul_def`, `one_def`, `ratio_inv`, `ratio_pow`, `ratio_refl`, `ratio_symm`, `ratio_toDilation`, `ratio_trans`, `ratio_zpow`, `refl_apply`, `refl_symm`, `refl_trans`, `self_trans_symm`, `surjective`, `symm_apply_apply`, `symm_bijective`, `symm_symm`, `symm_trans_self`, `toHomeomorph_symm`, `toPerm_apply`, `trans_apply`, `trans_refl`, `edist_eq'`, `coe_symm_toDilationEquiv`, `coe_toDilationEquiv`, `toDilationEquiv_apply`, `toDilationEquiv_ratio`, `toDilationEquiv_symm`, `toDilationEquiv_toDilation`, `instDilationClassOfDilationEquivClass`	46
Total	60

DilationEquiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	35 math math: `coe_toHomeomorph`, `smulTorsor_symm_apply`, `IsometryEquiv.toDilationEquiv_ratio`, `coe_one`, `coe_symm_toHomeomorph`, `trans_apply`, `bijective`, `coe_toEquiv`, `ext_iff`, `mulRight_symm_apply`, `symm_apply_apply`, `mulLeft_symm_apply`, `mulLeft_apply`, `ratio_inv`, `ratio_zpow`, `smulTorsor_apply`, `mulRight_apply`, `ratio_toDilation`, `instDilationEquivClass`, `injective`, `ratio_trans`, `ratio_refl`, `apply_symm_apply`, `IsometryEquiv.toDilationEquiv_apply`, `smulTorsor_ratio`, `refl_apply`, `coe_mul`, `surjective`, `IsometryEquiv.coe_symm_toDilationEquiv`, `coe_inv`, `smulTorsor_preimage_ball`, `coe_pow`, `ratio_symm`, `IsometryEquiv.coe_toDilationEquiv`, `ratio_pow`
`instGroup` 📖	CompOp	11 math math: `toPerm_apply`, `coe_one`, `ratio_inv`, `ratio_zpow`, `mul_def`, `one_def`, `coe_mul`, `inv_def`, `coe_inv`, `coe_pow`, `ratio_pow`
`ratioHom` 📖	CompOp	—
`refl` 📖	CompOp	8 math math: `refl_symm`, `trans_refl`, `ratio_refl`, `refl_trans`, `self_trans_symm`, `refl_apply`, `one_def`, `symm_trans_self`
`toDilation` 📖	CompOp	2 math math: `ratio_toDilation`, `IsometryEquiv.toDilationEquiv_toDilation`
`toEquiv` 📖	CompOp	3 math math: `toPerm_apply`, `edist_eq'`, `coe_toEquiv`
`toHomeomorph` 📖	CompOp	3 math math: `coe_toHomeomorph`, `coe_symm_toHomeomorph`, `toHomeomorph_symm`
`toPerm` 📖	CompOp	1 math math: `toPerm_apply`
`trans` 📖	CompOp	7 math math: `trans_apply`, `trans_refl`, `ratio_trans`, `refl_trans`, `mul_def`, `self_trans_symm`, `symm_trans_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.right_inv`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.bijective`
`coe_inv` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `symm`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `Nat.iterate`	—	`coe_toEquiv` `toPerm_apply` `map_pow` `MonoidHom.instMonoidHomClass` `Equiv.Perm.coe_pow`
`coe_symm_toHomeomorph` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorph` `DilationEquiv` `instEquivLike` `symm`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `DilationEquiv` `instEquivLike`	—	—
`coe_toHomeomorph` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorph` `DilationEquiv` `instEquivLike`	—	—
`edist_eq'` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `Equiv.toFun` `toEquiv` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	—
`ext` 📖	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`injective` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.injective`
`instDilationEquivClass` 📖	mathematical	—	`DilationEquivClass` `DilationEquiv` `instEquivLike`	—	`edist_eq'`
`inv_def` 📖	mathematical	—	`DilationEquiv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `symm`	—	—
`map_cobounded` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `EquivLike.toFunLike` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`Dilation.comap_cobounded` `instDilationClassOfDilationEquivClass` `Filter.map_comap_of_surjective` `EquivLike.surjective`
`mul_def` 📖	mathematical	—	`DilationEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `trans`	—	—
`one_def` 📖	mathematical	—	`DilationEquiv` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `refl`	—	—
`ratio_inv` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `NNReal` `NNReal.instInv`	—	`ratio_symm`
`ratio_pow` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `NNReal` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	`MonoidHom.map_pow`
`ratio_refl` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `refl` `NNReal` `instOneNNReal`	—	`Dilation.ratio_id`
`ratio_symm` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `symm` `NNReal` `NNReal.instInv`	—	`eq_inv_of_mul_eq_one_left` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `ratio_trans` `symm_trans_self` `ratio_refl`
`ratio_toDilation` 📖	mathematical	—	`Dilation.ratio` `Dilation` `Dilation.funLike` `Dilation.toDilationClass` `toDilation` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass`	—	`Dilation.toDilationClass`
`ratio_trans` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `trans` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`instDilationClassOfDilationEquivClass` `instDilationEquivClass` `Function.Surjective.forall₂` `surjective` `Dilation.edist_eq` `MulZeroClass.mul_zero` `ENNReal.mul_top` `Dilation.ratio_of_trivial` `mul_one` `Dilation.toDilationClass` `Dilation.ratio_comp'` `Mathlib.Tactic.Push.not_forall_eq` `mul_comm`
`ratio_zpow` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `instDilationClassOfDilationEquivClass` `instDilationEquivClass` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instGroup` `NNReal` `NNReal.zpow`	—	`MonoidHom.map_zpow`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	—
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_apply_apply`
`surjective` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.left_inv`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `DilationEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `apply_symm_apply`
`toHomeomorph_symm` 📖	mathematical	—	`toHomeomorph` `symm` `Homeomorph.symm` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	—
`toPerm_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `DilationEquiv` `Equiv.Perm` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `toPerm` `toEquiv`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	—

DilationEquiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

DilationEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist_eq'` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `EquivLike.toFunLike` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	—

IsometryEquiv

Definitions

Name	Category	Theorems
`toDilationEquiv` 📖	CompOp	6 math math: `toDilationEquiv_symm`, `toDilationEquiv_ratio`, `toDilationEquiv_toDilation`, `toDilationEquiv_apply`, `coe_symm_toDilationEquiv`, `coe_toDilationEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_symm_toDilationEquiv` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `DilationEquiv.instEquivLike` `DilationEquiv.symm` `toDilationEquiv` `IsometryEquiv` `instEquivLike` `symm`	—	—
`coe_toDilationEquiv` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `DilationEquiv.instEquivLike` `toDilationEquiv` `IsometryEquiv` `instEquivLike`	—	—
`toDilationEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EquivLike.toFunLike` `DilationEquiv.instEquivLike` `toDilationEquiv` `IsometryEquiv` `instEquivLike`	—	—
`toDilationEquiv_ratio` 📖	mathematical	—	`Dilation.ratio` `DilationEquiv` `EquivLike.toFunLike` `DilationEquiv.instEquivLike` `instDilationClassOfDilationEquivClass` `DilationEquiv.instDilationEquivClass` `toDilationEquiv` `NNReal` `instOneNNReal`	—	`instDilationClassOfDilationEquivClass` `DilationEquiv.instDilationEquivClass` `Dilation.toDilationClass` `DilationEquiv.ratio_toDilation` `isometry` `toDilationEquiv_toDilation` `Isometry.toDilation_ratio`
`toDilationEquiv_symm` 📖	mathematical	—	`toDilationEquiv` `symm` `DilationEquiv.symm`	—	—
`toDilationEquiv_toDilation` 📖	mathematical	—	`DilationEquiv.toDilation` `toDilationEquiv` `Isometry.toDilation` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `isometry`	—	—

(root)

Definitions

Name	Category	Theorems
`DilationEquiv` 📖	CompData	40 math math: `DilationEquiv.toPerm_apply`, `DilationEquiv.coe_toHomeomorph`, `DilationEquiv.smulTorsor_symm_apply`, `IsometryEquiv.toDilationEquiv_ratio`, `DilationEquiv.coe_one`, `DilationEquiv.coe_symm_toHomeomorph`, `DilationEquiv.trans_apply`, `DilationEquiv.symm_bijective`, `DilationEquiv.bijective`, `DilationEquiv.coe_toEquiv`, `DilationEquiv.ext_iff`, `DilationEquiv.mulRight_symm_apply`, `DilationEquiv.symm_apply_apply`, `DilationEquiv.mulLeft_symm_apply`, `DilationEquiv.mulLeft_apply`, `DilationEquiv.ratio_inv`, `DilationEquiv.ratio_zpow`, `DilationEquiv.smulTorsor_apply`, `DilationEquiv.mulRight_apply`, `DilationEquiv.ratio_toDilation`, `DilationEquiv.instDilationEquivClass`, `DilationEquiv.injective`, `DilationEquiv.ratio_trans`, `DilationEquiv.ratio_refl`, `DilationEquiv.apply_symm_apply`, `IsometryEquiv.toDilationEquiv_apply`, `DilationEquiv.smulTorsor_ratio`, `DilationEquiv.mul_def`, `DilationEquiv.refl_apply`, `DilationEquiv.one_def`, `DilationEquiv.coe_mul`, `DilationEquiv.surjective`, `IsometryEquiv.coe_symm_toDilationEquiv`, `DilationEquiv.inv_def`, `DilationEquiv.coe_inv`, `DilationEquiv.smulTorsor_preimage_ball`, `DilationEquiv.coe_pow`, `DilationEquiv.ratio_symm`, `IsometryEquiv.coe_toDilationEquiv`, `DilationEquiv.ratio_pow`
`DilationEquivClass` 📖	CompData	1 math math: `DilationEquiv.instDilationEquivClass`
`«term_≃ᵈ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instDilationClassOfDilationEquivClass` 📖	mathematical	—	`DilationClass` `EquivLike.toFunLike`	—	`DilationEquivClass.edist_eq'`

---

← Back to Index