Dilation

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

Statistics

Metric	Count
Definitions `Dilation`, `comp`, `copy`, `funLike`, `id`, `instInhabited`, `instMonoid`, `mkOfDistEq`, `mkOfNNDistEq`, `ratio`, `ratioHom`, `toFun`, `DilationClass`, `toDilation`, `«term_→ᵈ_»`	15
Theorems `antilipschitz`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_id`, `coe_mk`, `coe_mkOfDistEq`, `coe_mkOfNNDistEq`, `coe_mul`, `coe_one`, `comap_cobounded`, `comp_apply`, `comp_assoc`, `comp_continuousOn_iff`, `comp_continuous_iff`, `comp_id`, `congr_arg`, `congr_fun`, `copy_eq_self`, `copy_toFun`, `diam_image`, `diam_range`, `dist_eq`, `ediam_image`, `ediam_range`, `edist_eq`, `edist_eq'`, `ext`, `ext_iff`, `id_comp`, `injective`, `isClosedEmbedding`, `isEmbedding`, `isUniformEmbedding`, `isUniformInducing`, `lipschitz`, `mapsTo_ball`, `mapsTo_closedBall`, `mapsTo_closedEBall`, `mapsTo_eball`, `mapsTo_emetric_ball`, `mapsTo_emetric_closedBall`, `mapsTo_sphere`, `mk_coe`, `mk_coe_of_dist_eq`, `mk_coe_of_nndist_eq`, `mul_def`, `nndist_eq`, `one_def`, `ratioHom_apply`, `ratio_comp`, `ratio_comp'`, `ratio_id`, `ratio_mul`, `ratio_ne_zero`, `ratio_of_subsingleton`, `ratio_of_trivial`, `ratio_one`, `ratio_pos`, `ratio_pow`, `ratio_unique`, `ratio_unique_of_dist_ne_zero`, `ratio_unique_of_nndist_ne_zero`, `tendsto_cobounded`, `tendsto_nhds_iff`, `toContinuous`, `toDilationClass`, `toFun_eq_coe`, `edist_eq'`, `toDilation_ratio`, `toDilation_toFun`	71
Total	86

Dilation

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	10 math math: `cancel_right`, `cancel_left`, `comp_apply`, `comp_id`, `coe_comp`, `id_comp`, `comp_assoc`, `mul_def`, `ratio_comp`, `ratio_comp'`
`copy` 📖	CompOp	2 math math: `copy_toFun`, `copy_eq_self`
`funLike` 📖	CompOp	25 math math: `ratio_one`, `coe_mk`, `ratio_id`, `ratio_mul`, `comp_apply`, `coe_mkOfNNDistEq`, `coe_comp`, `ratioHom_apply`, `Isometry.toDilation_ratio`, `ratio_pow`, `coe_one`, `toFun_eq_coe`, `coe_mul`, `DilationEquiv.ratio_toDilation`, `coe_id`, `congr_fun`, `coe_mkOfDistEq`, `ratio_comp`, `ratio_comp'`, `mulRight_toFun`, `ext_iff`, `toDilationClass`, `mulLeft_toFun`, `Isometry.toDilation_toFun`, `congr_arg`
`id` 📖	CompOp	5 math math: `ratio_id`, `comp_id`, `id_comp`, `coe_id`, `one_def`
`instInhabited` 📖	CompOp	—
`instMonoid` 📖	CompOp	8 math math: `ratio_one`, `ratio_mul`, `ratioHom_apply`, `ratio_pow`, `coe_one`, `coe_mul`, `mul_def`, `one_def`
`mkOfDistEq` 📖	CompOp	2 math math: `coe_mkOfDistEq`, `mk_coe_of_dist_eq`
`mkOfNNDistEq` 📖	CompOp	2 math math: `mk_coe_of_nndist_eq`, `coe_mkOfNNDistEq`
`ratio` 📖	CompOp	39 math math: `ratio_one`, `mapsTo_eball`, `mapsTo_closedEBall`, `ratio_unique_of_dist_ne_zero`, `mapsTo_sphere`, `antilipschitz`, `ratio_id`, `IsometryEquiv.toDilationEquiv_ratio`, `ratio_mul`, `ediam_range`, `nndist_eq`, `ratioHom_apply`, `edist_eq`, `mapsTo_closedBall`, `ratio_unique`, `mapsTo_emetric_closedBall`, `Isometry.toDilation_ratio`, `DilationEquiv.ratio_inv`, `DilationEquiv.ratio_zpow`, `ratio_pow`, `ratio_pos`, `DilationEquiv.ratio_toDilation`, `mapsTo_ball`, `DilationEquiv.ratio_trans`, `DilationEquiv.ratio_refl`, `ratio_comp`, `DilationEquiv.smulTorsor_ratio`, `diam_range`, `diam_image`, `ratio_comp'`, `lipschitz`, `mapsTo_emetric_ball`, `ediam_image`, `dist_eq`, `ratio_unique_of_nndist_ne_zero`, `ratio_of_trivial`, `DilationEquiv.ratio_symm`, `DilationEquiv.ratio_pow`, `ratio_of_subsingleton`
`ratioHom` 📖	CompOp	1 math math: `ratioHom_apply`
`toFun` 📖	CompOp	2 math math: `edist_eq'`, `toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitz` 📖	mathematical	—	`AntilipschitzWith` `NNReal` `NNReal.instInv` `ratio` `DFunLike.coe`	—	`ratio_ne_zero` `ENNReal.mul_le_iff_le_inv` `ENNReal.coe_ne_zero` `ENNReal.coe_ne_top` `Eq.ge` `edist_eq`
`cancel_left` 📖	mathematical	`DFunLike.coe` `Dilation` `funLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `Dilation` `funLike`	`comp`	—	`ext` `Function.Surjective.forall` `ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike` `comp`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike` `id`	—	—
`coe_mk` 📖	mathematical	`EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	`DFunLike.coe` `Dilation` `funLike`	—	—
`coe_mkOfDistEq` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instMul` `NNReal.toReal`	`DFunLike.coe` `Dilation` `PseudoMetricSpace.toPseudoEMetricSpace` `funLike` `mkOfDistEq`	—	—
`coe_mkOfNNDistEq` 📖	mathematical	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`DFunLike.coe` `Dilation` `PseudoMetricSpace.toPseudoEMetricSpace` `funLike` `mkOfNNDistEq`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`comap_cobounded` 📖	mathematical	—	`Filter.comap` `DFunLike.coe` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`le_antisymm` `LipschitzWith.comap_cobounded_le` `lipschitz` `Filter.Tendsto.le_comap` `tendsto_cobounded`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_continuousOn_iff` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe`	—	`Topology.IsInducing.continuousOn_iff` `IsUniformInducing.isInducing` `isUniformInducing`
`comp_continuous_iff` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe`	—	`Topology.IsInducing.continuous_iff` `IsUniformInducing.isInducing` `isUniformInducing`
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike`	—	`DFunLike.congr_fun`
`copy_eq_self` 📖	mathematical	`DFunLike.coe` `Dilation` `funLike`	`copy`	—	`DFunLike.ext'`
`copy_toFun` 📖	mathematical	`DFunLike.coe` `Dilation` `funLike`	`copy`	—	—
`diam_image` 📖	mathematical	—	`Metric.diam` `Set.image` `DFunLike.coe` `Real` `Real.instMul` `NNReal.toReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`ediam_image` `ENNReal.toReal_mul`
`diam_range` 📖	mathematical	—	`Metric.diam` `Set.range` `DFunLike.coe` `Real` `Real.instMul` `NNReal.toReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.univ`	—	`Set.image_univ` `diam_image`
`dist_eq` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Real` `Real.instMul` `NNReal.toReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`nndist_eq`
`ediam_image` 📖	mathematical	—	`Metric.ediam` `Set.image` `DFunLike.coe` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio`	—	`LE.le.antisymm` `LipschitzWith.ediam_image_le` `lipschitz` `ENNReal.mul_le_of_le_div'` `div_eq_mul_inv` `mul_comm` `ENNReal.coe_inv` `ratio_ne_zero` `AntilipschitzWith.le_mul_ediam_image` `antilipschitz`
`ediam_range` 📖	mathematical	—	`Metric.ediam` `Set.range` `DFunLike.coe` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio` `Set.univ`	—	`Set.image_univ` `ediam_image`
`edist_eq` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio`	—	`DilationClass.edist_eq'` `ratio.eq_1` `MulZeroClass.mul_zero` `ENNReal.mul_top` `one_mul`
`edist_eq'` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `toFun` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	—
`ext` 📖	—	`DFunLike.coe` `Dilation` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Dilation` `funLike`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`injective` 📖	mathematical	—	`DFunLike.coe`	—	`AntilipschitzWith.injective` `antilipschitz`
`isClosedEmbedding` 📖	mathematical	—	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `DFunLike.coe`	—	`AntilipschitzWith.isClosedEmbedding` `antilipschitz` `LipschitzWith.uniformContinuous` `lipschitz`
`isEmbedding` 📖	mathematical	—	`Topology.IsEmbedding` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `DFunLike.coe`	—	`IsUniformEmbedding.isEmbedding` `isUniformEmbedding`
`isUniformEmbedding` 📖	mathematical	—	`IsUniformEmbedding` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `DFunLike.coe`	—	`AntilipschitzWith.isUniformEmbedding` `antilipschitz` `LipschitzWith.uniformContinuous` `lipschitz`
`isUniformInducing` 📖	mathematical	—	`IsUniformInducing` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe`	—	`AntilipschitzWith.isUniformInducing` `antilipschitz` `LipschitzWith.uniformContinuous` `lipschitz`
`lipschitz` 📖	mathematical	—	`LipschitzWith` `ratio` `DFunLike.coe`	—	`Eq.le` `edist_eq`
`mapsTo_ball` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.ball` `Real` `Real.instMul` `NNReal.toReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Eq.trans_lt` `dist_eq` `mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ratio_pos`
`mapsTo_closedBall` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.closedBall` `Real` `Real.instMul` `NNReal.toReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Eq.trans_le` `dist_eq` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg`
`mapsTo_closedEBall` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.closedEBall` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio`	—	`Eq.trans_le` `edist_eq` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`mapsTo_eball` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.eball` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio`	—	`Metric.mem_eball` `edist_eq` `ENNReal.mul_lt_mul_right`
`mapsTo_emetric_ball` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.eball` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio`	—	`mapsTo_eball`
`mapsTo_emetric_closedBall` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.closedEBall` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `ratio`	—	`mapsTo_closedEBall`
`mapsTo_sphere` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Metric.sphere` `Real` `Real.instMul` `NNReal.toReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`dist_eq` `Metric.mem_sphere`
`mk_coe` 📖	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Dilation` `funLike` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	—	`ext`
`mk_coe_of_dist_eq` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Dilation` `PseudoMetricSpace.toPseudoEMetricSpace` `funLike` `Real` `Real.instMul` `NNReal.toReal`	`mkOfDistEq`	—	`ext`
`mk_coe_of_nndist_eq` 📖	mathematical	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `Dilation` `PseudoMetricSpace.toPseudoEMetricSpace` `funLike` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`mkOfNNDistEq`	—	`ext`
`mul_def` 📖	mathematical	—	`Dilation` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `comp`	—	—
`nndist_eq` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`edist_eq`
`one_def` 📖	mathematical	—	`Dilation` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `id`	—	—
`ratioHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Dilation` `NNReal` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidHom.instFunLike` `ratioHom` `ratio` `funLike` `toDilationClass`	—	—
`ratio_comp` 📖	mathematical	—	`ratio` `Dilation` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `funLike` `toDilationClass` `comp` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`ratio_comp'` `exists_pair_ne` `edist_eq_zero` `edist_ne_top`
`ratio_comp'` 📖	mathematical	—	`ratio` `Dilation` `funLike` `toDilationClass` `comp` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`toDilationClass` `edist_eq` `ENNReal.coe_mul`
`ratio_id` 📖	mathematical	—	`ratio` `Dilation` `funLike` `toDilationClass` `id` `NNReal` `instOneNNReal`	—	`toDilationClass` `DilationClass.edist_eq'` `ratio.eq_1` `Mathlib.Tactic.Push.not_forall_eq` `ratio_unique` `one_mul`
`ratio_mul` 📖	mathematical	—	`ratio` `Dilation` `funLike` `toDilationClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`toDilationClass` `ratio_of_trivial` `mul_one` `ratio_comp'` `Mathlib.Tactic.Push.not_forall_eq`
`ratio_ne_zero` 📖	—	—	—	—	`DilationClass.edist_eq'` `ratio.eq_1` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`
`ratio_of_subsingleton` 📖	mathematical	—	`ratio` `NNReal` `instOneNNReal`	—	`PseudoEMetricSpace.edist_self` `DilationClass.edist_eq'`
`ratio_of_trivial` 📖	mathematical	`EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal` `instZeroENNReal` `Top.top` `instTopENNReal`	`ratio` `NNReal` `instOneNNReal`	—	`DilationClass.edist_eq'`
`ratio_one` 📖	mathematical	—	`ratio` `Dilation` `funLike` `toDilationClass` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `NNReal` `instOneNNReal`	—	`ratio_id`
`ratio_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ratio`	—	`Ne.bot_lt` `ratio_ne_zero`
`ratio_pow` 📖	mathematical	—	`ratio` `Dilation` `funLike` `toDilationClass` `Monoid.toNatPow` `instMonoid` `NNReal` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	`MonoidHom.map_pow`
`ratio_unique` 📖	mathematical	`EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	`ratio`	—	`edist_eq`
`ratio_unique_of_dist_ne_zero` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `Real` `Real.instMul` `NNReal.toReal`	`ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`ratio_unique_of_nndist_ne_zero` `NNReal.coe_ne_zero` `NNReal.eq` `coe_nndist` `NNReal.coe_mul`
`ratio_unique_of_nndist_ne_zero` 📖	mathematical	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`ratio` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`ratio_unique` `edist_nndist` `ENNReal.coe_ne_zero` `edist_ne_top` `ENNReal.coe_mul`
`tendsto_cobounded` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`AntilipschitzWith.tendsto_cobounded` `antilipschitz`
`tendsto_nhds_iff` 📖	mathematical	—	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe`	—	`Topology.IsInducing.tendsto_nhds_iff` `IsUniformInducing.isInducing` `isUniformInducing`
`toContinuous` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe`	—	`LipschitzWith.continuous` `lipschitz`
`toDilationClass` 📖	mathematical	—	`DilationClass` `Dilation` `funLike`	—	`edist_eq'`
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `Dilation` `funLike`	—	—

DilationClass

Theorems

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

Isometry

Definitions

Name	Category	Theorems
`toDilation` 📖	CompOp	3 math math: `toDilation_ratio`, `IsometryEquiv.toDilationEquiv_toDilation`, `toDilation_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toDilation_ratio` 📖	mathematical	`Isometry`	`Dilation.ratio` `Dilation` `Dilation.funLike` `Dilation.toDilationClass` `toDilation` `NNReal` `instOneNNReal`	—	`Dilation.toDilationClass` `Dilation.ratio_of_trivial` `Mathlib.Tactic.Push.not_forall_eq` `Dilation.ratio_unique` `one_mul`
`toDilation_toFun` 📖	mathematical	`Isometry`	`DFunLike.coe` `Dilation` `Dilation.funLike` `toDilation`	—	—

(root)

Definitions

Name	Category	Theorems
`Dilation` 📖	CompData	27 math math: `Dilation.ratio_one`, `Dilation.coe_mk`, `Dilation.ratio_id`, `Dilation.ratio_mul`, `Dilation.comp_apply`, `Dilation.coe_mkOfNNDistEq`, `Dilation.coe_comp`, `Dilation.ratioHom_apply`, `Isometry.toDilation_ratio`, `Dilation.ratio_pow`, `Dilation.coe_one`, `Dilation.toFun_eq_coe`, `Dilation.coe_mul`, `DilationEquiv.ratio_toDilation`, `Dilation.coe_id`, `Dilation.mul_def`, `Dilation.congr_fun`, `Dilation.coe_mkOfDistEq`, `Dilation.ratio_comp`, `Dilation.one_def`, `Dilation.ratio_comp'`, `Dilation.mulRight_toFun`, `Dilation.ext_iff`, `Dilation.toDilationClass`, `Dilation.mulLeft_toFun`, `Isometry.toDilation_toFun`, `Dilation.congr_arg`
`DilationClass` 📖	CompData	2 math math: `instDilationClassOfDilationEquivClass`, `Dilation.toDilationClass`
`«term_→ᵈ_»` 📖	CompOp	—

---

← Back to Index