Isometry

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

Statistics

Metric	Count
Definitions `appendIsometry`, `appendIsometryOfEq`, `Isometry`, `isometryEquivOnRange`, `IsometryClass`, `instCoeOutIsometryEquiv`, `toIsometryEquiv`, `apply`, `symm_apply`, `funUnique`, `instEquivLike`, `instGroup`, `mk'`, `piCongrLeft`, `piCongrLeft'`, `piFinTwo`, `refl`, `sumArrowIsometryEquivProdArrow`, `toEquiv`, `toHomeomorph`, `trans`, `Isometry`, `«term_≃ᵢ_»`	23
Theorems `isometry_induced`, `appendIsometryOfEq_apply`, `appendIsometryOfEq_symm_apply`, `appendIsometry_apply`, `appendIsometry_symm_apply`, `appendIsometry_toHomeomorph`, `edist_append_eq_max_edist`, `to_isometry`, `antilipschitz`, `comp`, `comp_continuousOn_iff`, `comp_continuous_iff`, `continuous`, `diam_image`, `diam_range`, `dist_eq`, `ediam_image`, `ediam_range`, `edist_eq`, `injective`, `inl`, `inr`, `isClosedEmbedding`, `isEmbedding`, `isUniformEmbedding`, `isUniformInducing`, `isometryEquivOnRange_apply`, `isometryEquivOnRange_toEquiv`, `lipschitz`, `lipschitzWith_iff`, `mapsTo_ball`, `mapsTo_closedBall`, `mapsTo_closedEBall`, `mapsTo_eball`, `mapsTo_emetric_ball`, `mapsTo_emetric_closedBall`, `mapsTo_sphere`, `nndist_eq`, `of_dist_eq`, `of_nndist_eq`, `piMap`, `preimage_ball`, `preimage_closedBall`, `preimage_closedEBall`, `preimage_eball`, `preimage_emetric_ball`, `preimage_emetric_closedBall`, `preimage_setOf_dist`, `preimage_sphere`, `prodMap`, `right_inv`, `single`, `tendsto_nhds_iff`, `uniformContinuous`, `antilipschitz`, `coe_coe`, `continuous`, `diam_image`, `diam_range`, `dist_eq`, `ediam_image`, `ediam_range`, `edist_eq`, `isometry`, `lipschitz`, `nndist_eq`, `toContinuousMapClass`, `toHomeomorphClass`, `toIsometryEquiv_injective`, `apply_inv_self`, `apply_symm_apply`, `bijective`, `coe_eq_toEquiv`, `coe_mk`, `coe_mul`, `coe_one`, `coe_symm_toEquiv`, `coe_toEquiv`, `coe_toHomeomorph`, `coe_toHomeomorph_symm`, `comp_continuousOn_iff`, `comp_continuous_iff`, `comp_continuous_iff'`, `completeSpace`, `completeSpace_iff`, `continuous`, `diam_image`, `diam_preimage`, `diam_univ`, `dist_eq`, `ediam_image`, `ediam_preimage`, `ediam_univ`, `edist_eq`, `eq_symm_apply`, `ext`, `ext_iff`, `funUnique_apply`, `funUnique_symm_apply`, `image_ball`, `image_closedBall`, `image_closedEBall`, `image_eball`, `image_emetric_ball`, `image_emetric_closedBall`, `image_sphere`, `image_symm`, `injective`, `instIsometryClass`, `inv_apply_self`, `isometry`, `isometry_toFun`, `mul_apply`, `nndist_eq`, `piCongrLeft'_apply`, `piCongrLeft'_symm_apply`, `piCongrLeft_apply`, `piCongrLeft_symm_apply`, `piFinTwo_apply`, `piFinTwo_symm_apply`, `preimage_ball`, `preimage_closedBall`, `preimage_closedEBall`, `preimage_eball`, `preimage_emetric_ball`, `preimage_emetric_closedBall`, `preimage_sphere`, `preimage_symm`, `range_eq_univ`, `self_comp_symm`, `sumArrowIsometryEquivProdArrow_apply`, `sumArrowIsometryEquivProdArrow_symm_apply`, `sumArrowIsometryEquivProdArrow_toHomeomorph`, `surjective`, `symm_apply_apply`, `symm_apply_eq`, `symm_bijective`, `symm_comp_self`, `symm_symm`, `symm_trans_apply`, `toEquiv_inj`, `toEquiv_injective`, `toEquiv_toHomeomorph`, `trans_apply`, `isometry_induced`, `isometry_induced`, `isometry_induced`, `to_isometry`, `isometry_id`, `isometry_iff_dist_eq`, `isometry_iff_nndist_eq`, `isometry_subsingleton`, `isometry_subtype_coe`	153
Total	176

EMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_induced` 📖	mathematical	—	`Isometry` `toPseudoEMetricSpace` `induced`	—	—

Fin

Definitions

Name	Category	Theorems
`appendIsometry` 📖	CompOp	3 math math: `appendIsometry_symm_apply`, `appendIsometry_toHomeomorph`, `appendIsometry_apply`
`appendIsometryOfEq` 📖	CompOp	2 math math: `appendIsometryOfEq_apply`, `appendIsometryOfEq_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`appendIsometryOfEq_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `Prod.pseudoEMetricSpaceMax` `pseudoEMetricSpacePi` `fintype` `EquivLike.toFunLike` `IsometryEquiv.instEquivLike` `appendIsometryOfEq` `append`	—	—
`appendIsometryOfEq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `fintype` `Prod.pseudoEMetricSpaceMax` `EquivLike.toFunLike` `IsometryEquiv.instEquivLike` `IsometryEquiv.symm` `appendIsometryOfEq`	—	—
`appendIsometry_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `Prod.pseudoEMetricSpaceMax` `pseudoEMetricSpacePi` `fintype` `EquivLike.toFunLike` `IsometryEquiv.instEquivLike` `appendIsometry` `append`	—	—
`appendIsometry_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `fintype` `Prod.pseudoEMetricSpaceMax` `EquivLike.toFunLike` `IsometryEquiv.instEquivLike` `IsometryEquiv.symm` `appendIsometry`	—	—
`appendIsometry_toHomeomorph` 📖	mathematical	—	`IsometryEquiv.toHomeomorph` `Prod.pseudoEMetricSpaceMax` `pseudoEMetricSpacePi` `fintype` `appendIsometry` `appendHomeomorph` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	—
`edist_append_eq_max_edist` 📖	mathematical	—	`EDist.edist` `instEDistForall` `fintype` `PseudoEMetricSpace.toEDist` `append` `ENNReal` `ENNReal.instMax`	—	`Finset.sup_univ_eq_iSup` `Equiv.iSup_comp` `iSup_sum` `append_left` `append_right`

IsUniformEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_isometry` 📖	mathematical	`IsUniformEmbedding` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `comapMetricSpace`	—	`Isometry.of_dist_eq`

Isometry

Definitions

Name	Category	Theorems
`isometryEquivOnRange` 📖	CompOp	2 math math: `isometryEquivOnRange_toEquiv`, `isometryEquivOnRange_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitz` 📖	mathematical	`Isometry`	`AntilipschitzWith` `NNReal` `instOneNNReal`	—	`one_mul`
`comp` 📖	—	`Isometry`	—	—	—
`comp_continuousOn_iff` 📖	mathematical	`Isometry`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Topology.IsInducing.continuousOn_iff` `IsUniformInducing.isInducing` `isUniformInducing`
`comp_continuous_iff` 📖	mathematical	`Isometry`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Topology.IsInducing.continuous_iff` `IsUniformInducing.isInducing` `isUniformInducing`
`continuous` 📖	mathematical	`Isometry`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`LipschitzWith.continuous` `lipschitz`
`diam_image` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Metric.diam` `Set.image`	—	`Metric.diam.eq_1` `ediam_image`
`diam_range` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Metric.diam` `Set.range` `Set.univ`	—	`Set.image_univ` `diam_image`
`dist_eq` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Dist.dist` `PseudoMetricSpace.toDist`	—	`isometry_iff_dist_eq`
`ediam_image` 📖	mathematical	`Isometry`	`Metric.ediam` `Set.image`	—	`eq_of_forall_ge_iff` `edist_eq`
`ediam_range` 📖	mathematical	`Isometry`	`Metric.ediam` `Set.range` `Set.univ`	—	`Set.image_univ` `ediam_image`
`edist_eq` 📖	mathematical	`Isometry`	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	—
`injective` 📖	—	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	—	—	`AntilipschitzWith.injective` `antilipschitz`
`inl` 📖	mathematical	—	`Isometry` `Prod.pseudoEMetricSpaceMax` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoidHom.instFunLike` `AddMonoidHom.inl`	—	`Prod.edist_eq` `PseudoEMetricSpace.edist_self` `sup_of_le_left` `ENNReal.instCanonicallyOrderedAdd`
`inr` 📖	mathematical	—	`Isometry` `Prod.pseudoEMetricSpaceMax` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoidHom.instFunLike` `AddMonoidHom.inr`	—	`Prod.edist_eq` `PseudoEMetricSpace.edist_self` `sup_of_le_right` `ENNReal.instCanonicallyOrderedAdd`
`isClosedEmbedding` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`AntilipschitzWith.isClosedEmbedding` `antilipschitz` `LipschitzWith.uniformContinuous` `lipschitz`
`isEmbedding` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`Topology.IsEmbedding` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`IsUniformEmbedding.isEmbedding` `isUniformEmbedding`
`isUniformEmbedding` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`IsUniformEmbedding` `PseudoEMetricSpace.toUniformSpace`	—	`AntilipschitzWith.isUniformEmbedding` `antilipschitz` `LipschitzWith.uniformContinuous` `lipschitz`
`isUniformInducing` 📖	mathematical	`Isometry`	`IsUniformInducing` `PseudoEMetricSpace.toUniformSpace`	—	`AntilipschitzWith.isUniformInducing` `antilipschitz` `uniformContinuous`
`isometryEquivOnRange_apply` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`DFunLike.coe` `IsometryEquiv` `Set.Elem` `Set.range` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `EquivLike.toFunLike` `IsometryEquiv.instEquivLike` `isometryEquivOnRange`	—	—
`isometryEquivOnRange_toEquiv` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`IsometryEquiv.toEquiv` `Set.Elem` `Set.range` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `isometryEquivOnRange` `Equiv.ofInjective` `injective`	—	—
`lipschitz` 📖	mathematical	`Isometry`	`LipschitzWith` `NNReal` `instOneNNReal`	—	`LipschitzWith.of_edist_le` `Eq.le`
`lipschitzWith_iff` 📖	mathematical	`Isometry`	`LipschitzWith`	—	`edist_eq`
`mapsTo_ball` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.MapsTo` `Metric.ball`	—	`Eq.ge` `preimage_ball`
`mapsTo_closedBall` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.MapsTo` `Metric.closedBall`	—	`Eq.ge` `preimage_closedBall`
`mapsTo_closedEBall` 📖	mathematical	`Isometry`	`Set.MapsTo` `Metric.closedEBall`	—	`Eq.ge` `preimage_closedEBall`
`mapsTo_eball` 📖	mathematical	`Isometry`	`Set.MapsTo` `Metric.eball`	—	`Eq.ge` `preimage_eball`
`mapsTo_emetric_ball` 📖	mathematical	`Isometry`	`Set.MapsTo` `Metric.eball`	—	`mapsTo_eball`
`mapsTo_emetric_closedBall` 📖	mathematical	`Isometry`	`Set.MapsTo` `Metric.closedEBall`	—	`mapsTo_closedEBall`
`mapsTo_sphere` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.MapsTo` `Metric.sphere`	—	`Eq.ge` `preimage_sphere`
`nndist_eq` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`isometry_iff_nndist_eq`
`of_dist_eq` 📖	mathematical	`Dist.dist` `PseudoMetricSpace.toDist`	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`isometry_iff_dist_eq`
`of_nndist_eq` 📖	mathematical	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`isometry_iff_nndist_eq`
`piMap` 📖	mathematical	`Isometry`	`pseudoEMetricSpacePi` `Pi.map`	—	`edist_eq`
`preimage_ball` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.preimage` `Metric.ball`	—	`preimage_setOf_dist`
`preimage_closedBall` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.preimage` `Metric.closedBall`	—	`preimage_setOf_dist`
`preimage_closedEBall` 📖	mathematical	`Isometry`	`Set.preimage` `Metric.closedEBall`	—	`Set.ext` `edist_eq`
`preimage_eball` 📖	mathematical	`Isometry`	`Set.preimage` `Metric.eball`	—	`Set.ext` `edist_eq`
`preimage_emetric_ball` 📖	mathematical	`Isometry`	`Set.preimage` `Metric.eball`	—	`preimage_eball`
`preimage_emetric_closedBall` 📖	mathematical	`Isometry`	`Set.preimage` `Metric.closedEBall`	—	`preimage_closedEBall`
`preimage_setOf_dist` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.preimage` `setOf` `Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_eq`
`preimage_sphere` 📖	mathematical	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.preimage` `Metric.sphere`	—	`preimage_setOf_dist`
`prodMap` 📖	mathematical	`Isometry`	`Prod.pseudoEMetricSpaceMax`	—	`edist_eq`
`right_inv` 📖	—	`Isometry`	—	—	—
`single` 📖	mathematical	—	`Isometry` `pseudoEMetricSpacePi` `Pi.single`	—	`edist_pi_def` `le_antisymm` `Finset.sup_le` `eq_or_ne` `Pi.single_eq_same` `Pi.single_eq_of_ne'` `PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd` `Finset.le_sup_of_le` `Finset.mem_univ`
`tendsto_nhds_iff` 📖	mathematical	`Isometry`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Topology.IsInducing.tendsto_nhds_iff` `IsUniformInducing.isInducing` `isUniformInducing`
`uniformContinuous` 📖	mathematical	`Isometry`	`UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	—	`LipschitzWith.uniformContinuous` `lipschitz`

IsometryClass

Definitions

Name	Category	Theorems
`instCoeOutIsometryEquiv` 📖	CompOp	—
`toIsometryEquiv` 📖	CompOp	2 math math: `toIsometryEquiv_injective`, `coe_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitz` 📖	mathematical	—	`AntilipschitzWith` `NNReal` `instOneNNReal` `DFunLike.coe`	—	`Isometry.antilipschitz` `isometry`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `IsometryEquiv.instEquivLike` `toIsometryEquiv`	—	—
`continuous` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe`	—	`Isometry.continuous` `isometry`
`diam_image` 📖	mathematical	—	`Metric.diam` `Set.image` `DFunLike.coe`	—	`Isometry.diam_image` `isometry`
`diam_range` 📖	mathematical	—	`Metric.diam` `Set.range` `DFunLike.coe` `Set.univ`	—	`Isometry.diam_range` `isometry`
`dist_eq` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe`	—	`Isometry.dist_eq` `isometry`
`ediam_image` 📖	mathematical	—	`Metric.ediam` `Set.image` `DFunLike.coe`	—	`Isometry.ediam_image` `isometry`
`ediam_range` 📖	mathematical	—	`Metric.ediam` `Set.range` `DFunLike.coe` `Set.univ`	—	`Isometry.ediam_range` `isometry`
`edist_eq` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe`	—	`Isometry.edist_eq` `isometry`
`isometry` 📖	mathematical	—	`Isometry` `DFunLike.coe`	—	—
`lipschitz` 📖	mathematical	—	`LipschitzWith` `NNReal` `instOneNNReal` `DFunLike.coe`	—	`Isometry.lipschitz` `isometry`
`nndist_eq` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe`	—	`Isometry.nndist_eq` `isometry`
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`continuous`
`toHomeomorphClass` 📖	mathematical	—	`HomeomorphClass` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`continuous` `Isometry.continuous` `Isometry.right_inv` `isometry` `EquivLike.right_inv`
`toIsometryEquiv_injective` 📖	mathematical	—	`IsometryEquiv` `toIsometryEquiv`	—	`DFunLike.ext` `DFunLike.congr_fun`

IsometryEquiv

Definitions

Name	Category	Theorems
`funUnique` 📖	CompOp	2 math math: `funUnique_apply`, `funUnique_symm_apply`
`instEquivLike` 📖	CompOp	122 math math: `image_sphere`, `image_emetric_closedBall`, `dimH_preimage`, `LinearIsometryEquiv.coe_symm_toIsometryEquiv`, `preimage_sphere`, `toRealLinearIsometryEquiv_symm_apply`, `range_eq_univ`, `apply_symm_apply`, `withLpUniqueProd_symm_apply`, `subLeft_symm_apply`, `toRealLinearIsometryEquiv_apply`, `withLpProdUnique_apply`, `neg_apply`, `preimage_emetric_closedBall`, `coe_toHomeomorph`, `inv_apply_self`, `piCongrLeft'_apply`, `constVSub_symm_apply`, `image_emetric_ball`, `divLeft_apply`, `subRight_apply`, `image_closedEBall`, `symm_apply_apply`, `Fin.appendIsometry_symm_apply`, `diam_image`, `edist_eq`, `hausdorffMeasure_image`, `ediam_preimage`, `Delone.DeloneSet.mapIsometry_symm_apply_carrier`, `preimage_emetric_ball`, `comp_continuousOn_iff`, `image_eball`, `ext_iff`, `Fin.appendIsometryOfEq_apply`, `divRight_apply`, `divLeft_symm_apply`, `instIsometryClass`, `preimage_closedEBall`, `mulLeft_apply`, `map_midpoint`, `addLeft_apply`, `LinearIsometryEquiv.coe_toIsometryEquiv`, `coe_withLpProdUnique`, `map_hausdorffMeasure`, `bijective`, `piFinTwo_symm_apply`, `hausdorffMeasure_preimage`, `sumArrowIsometryEquivProdArrow_symm_apply`, `withLpProdCongr_apply`, `piCongrLeft_symm_apply`, `ediam_image`, `Isometry.isometryEquivOnRange_apply`, `measurePreserving_hausdorffMeasure`, `funUnique_apply`, `coe_withLpUniqueProd`, `dimH_image`, `diam_preimage`, `toDilationEquiv_toDilation`, `apply_inv_self`, `coe_eq_toEquiv`, `AffineIsometryEquiv.coe_toIsometryEquiv`, `MeasureTheory.OuterMeasure.isometryEquiv_map_mkMetric`, `addRight_apply`, `comp_continuous_iff'`, `piCongrLeft_apply`, `coe_toEquiv`, `Fin.appendIsometryOfEq_symm_apply`, `image_closedBall`, `dist_eq`, `vaddConst_apply`, `withLpProdUnique_symm_apply`, `piCongrLeft'_symm_apply`, `withLpProdAssoc_apply`, `withLpUniqueProd_apply`, `symm_apply_eq`, `toDilationEquiv_apply`, `funUnique_symm_apply`, `constVSub_apply`, `coe_mul`, `coeFn_toRealAffineIsometryEquiv`, `coe_symm_toEquiv`, `eq_symm_apply`, `injective`, `constVAdd_apply`, `constSMul_apply`, `image_symm`, `vaddConst_symm_apply`, `piFinTwo_apply`, `coe_one`, `coe_symm_toDilationEquiv`, `Fin.appendIsometry_apply`, `symm_comp_self`, `mul_apply`, `image_ball`, `withLpProdAssoc_symm_apply`, `ContinuousMap.isometryEquivBoundedOfCompact_symm_apply`, `AffineIsometryEquiv.coe_symm_toIsometryEquiv`, `nndist_eq`, `mulRight_apply`, `subLeft_apply`, `coe_mk`, `withLpProdCongr_symm_apply`, `withLpProdComm_apply`, `ContinuousMap.isometryEquivBoundedOfCompact_apply`, `continuous`, `preimage_symm`, `sumArrowIsometryEquivProdArrow_apply`, `preimage_closedBall`, `preimage_ball`, `coe_toDilationEquiv`, `coe_toHomeomorph_symm`, `symm_trans_apply`, `isometry`, `surjective`, `preimage_eball`, `inv_apply`, `trans_apply`, `Delone.DeloneSet.mapIsometry_apply_carrier`, `self_comp_symm`, `comp_continuous_iff`, `MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric`, `IsometryClass.coe_coe`
`instGroup` 📖	CompOp	5 math math: `inv_apply_self`, `apply_inv_self`, `coe_mul`, `coe_one`, `mul_apply`
`mk'` 📖	CompOp	—
`piCongrLeft` 📖	CompOp	2 math math: `piCongrLeft_symm_apply`, `piCongrLeft_apply`
`piCongrLeft'` 📖	CompOp	4 math math: `piCongrLeft'_apply`, `piCongrLeft_symm_apply`, `piCongrLeft_apply`, `piCongrLeft'_symm_apply`
`piFinTwo` 📖	CompOp	2 math math: `piFinTwo_symm_apply`, `piFinTwo_apply`
`refl` 📖	CompOp	2 math math: `AffineIsometryEquiv.toIsometryEquiv_refl`, `Delone.DeloneSet.mapIsometry_refl`
`sumArrowIsometryEquivProdArrow` 📖	CompOp	3 math math: `sumArrowIsometryEquivProdArrow_toHomeomorph`, `sumArrowIsometryEquivProdArrow_symm_apply`, `sumArrowIsometryEquivProdArrow_apply`
`toEquiv` 📖	CompOp	21 math math: `neg_toEquiv`, `toEquiv_inj`, `constVAdd_toEquiv`, `constSMul_toEquiv`, `mulRight_toEquiv`, `divLeft_toEquiv`, `Isometry.isometryEquivOnRange_toEquiv`, `subLeft_toEquiv`, `inv_toEquiv`, `coe_eq_toEquiv`, `coe_toEquiv`, `isometry_toFun`, `toEquiv_injective`, `ContinuousMap.isometryEquivBoundedOfCompact_toEquiv`, `coe_symm_toEquiv`, `subRight_toEquiv`, `addRight_toEquiv`, `toEquiv_toHomeomorph`, `mulLeft_toEquiv`, `divRight_toEquiv`, `addLeft_toEquiv`
`toHomeomorph` 📖	CompOp	5 math math: `sumArrowIsometryEquivProdArrow_toHomeomorph`, `coe_toHomeomorph`, `Fin.appendIsometry_toHomeomorph`, `toEquiv_toHomeomorph`, `coe_toHomeomorph_symm`
`trans` 📖	CompOp	4 math math: `Delone.DeloneSet.mapIsometry_trans`, `LinearIsometryEquiv.toIsometryEquiv_trans`, `symm_trans_apply`, `trans_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_inv_self` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	`apply_symm_apply`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.bijective`
`coe_eq_toEquiv` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike` `toEquiv`	—	—
`coe_mk` 📖	mathematical	`Isometry` `Equiv.toFun`	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	—
`coe_symm_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `IsometryEquiv` `instEquivLike` `symm`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `IsometryEquiv` `instEquivLike`	—	—
`coe_toHomeomorph` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorph` `IsometryEquiv` `instEquivLike`	—	—
`coe_toHomeomorph_symm` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorph` `IsometryEquiv` `instEquivLike` `symm`	—	—
`comp_continuousOn_iff` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Homeomorph.comp_continuousOn_iff`
`comp_continuous_iff` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Homeomorph.comp_continuous_iff`
`comp_continuous_iff'` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Homeomorph.comp_continuous_iff'`
`completeSpace` 📖	mathematical	—	`CompleteSpace` `PseudoEMetricSpace.toUniformSpace`	—	`completeSpace_iff`
`completeSpace_iff` 📖	mathematical	—	`CompleteSpace` `PseudoEMetricSpace.toUniformSpace`	—	`range_eq_univ` `isComplete_image_iff` `Isometry.isUniformInducing` `isometry`
`continuous` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.continuous` `isometry`
`diam_image` 📖	mathematical	—	`Metric.diam` `Set.image` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.diam_image` `isometry`
`diam_preimage` 📖	mathematical	—	`Metric.diam` `Set.preimage` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `diam_image`
`diam_univ` 📖	mathematical	—	`Metric.diam` `Set.univ`	—	`ediam_univ`
`dist_eq` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.dist_eq` `isometry`
`ediam_image` 📖	mathematical	—	`Metric.ediam` `Set.image` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.ediam_image` `isometry`
`ediam_preimage` 📖	mathematical	—	`Metric.ediam` `Set.preimage` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `ediam_image`
`ediam_univ` 📖	mathematical	—	`Metric.ediam` `Set.univ`	—	`range_eq_univ` `Isometry.ediam_range` `isometry`
`edist_eq` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.edist_eq` `isometry`
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_apply`
`ext` 📖	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `EquivLike.toFunLike` `instEquivLike` `funUnique` `Unique.instInhabited`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `EquivLike.toFunLike` `instEquivLike` `symm` `funUnique`	—	—
`image_ball` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `Metric.ball`	—	`preimage_symm` `preimage_ball` `symm_symm`
`image_closedBall` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `Metric.closedBall`	—	`preimage_symm` `preimage_closedBall` `symm_symm`
`image_closedEBall` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.closedEBall`	—	`preimage_symm` `preimage_closedEBall` `symm_symm`
`image_eball` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.eball`	—	`preimage_symm` `preimage_eball` `symm_symm`
`image_emetric_ball` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.eball`	—	`image_eball`
`image_emetric_closedBall` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.closedEBall`	—	`image_closedEBall`
`image_sphere` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `Metric.sphere`	—	`preimage_symm` `preimage_sphere` `symm_symm`
`image_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.preimage`	—	`Set.image_eq_preimage_of_inverse` `Equiv.left_inv` `Equiv.right_inv`
`injective` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.injective`
`instIsometryClass` 📖	mathematical	—	`IsometryClass` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`isometry_toFun`
`inv_apply_self` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	`symm_apply_apply`
`isometry` 📖	mathematical	—	`Isometry` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`isometry_toFun`
`isometry_toFun` 📖	mathematical	—	`Isometry` `Equiv.toFun` `toEquiv`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	—
`nndist_eq` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.nndist_eq` `isometry`
`piCongrLeft'_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instEquivLike` `piCongrLeft'`	—	—
`piCongrLeft'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instEquivLike` `symm` `piCongrLeft'` `Equiv.symm_apply_apply`	—	—
`piCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft` `symm` `piCongrLeft'` `Equiv.symm`	—	—
`piCongrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `symm` `piCongrLeft` `piCongrLeft'` `Equiv.symm`	—	—
`piFinTwo_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `Fin.fintype` `Prod.pseudoEMetricSpaceMax` `EquivLike.toFunLike` `instEquivLike` `piFinTwo`	—	—
`piFinTwo_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `Prod.pseudoEMetricSpaceMax` `pseudoEMetricSpacePi` `Fin.fintype` `EquivLike.toFunLike` `instEquivLike` `symm` `piFinTwo` `Fin.cons` `finZeroElim`	—	—
`preimage_ball` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `Metric.ball` `symm`	—	`Isometry.preimage_ball` `isometry` `apply_symm_apply`
`preimage_closedBall` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `Metric.closedBall` `symm`	—	`Isometry.preimage_closedBall` `isometry` `apply_symm_apply`
`preimage_closedEBall` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.closedEBall` `symm`	—	`Isometry.preimage_closedEBall` `isometry` `apply_symm_apply`
`preimage_eball` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.eball` `symm`	—	`Isometry.preimage_eball` `isometry` `apply_symm_apply`
`preimage_emetric_ball` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.eball` `symm`	—	`preimage_eball`
`preimage_emetric_closedBall` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Metric.closedEBall` `symm`	—	`preimage_closedEBall`
`preimage_sphere` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `PseudoMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `Metric.sphere` `symm`	—	`Isometry.preimage_sphere` `isometry` `apply_symm_apply`
`preimage_symm` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.image`	—	`Set.image_eq_preimage_of_inverse` `Equiv.left_inv` `Equiv.right_inv`
`range_eq_univ` 📖	mathematical	—	`Set.range` `DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `Set.univ`	—	`EquivLike.range_eq_univ`
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.right_inv`
`sumArrowIsometryEquivProdArrow_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `pseudoEMetricSpacePi` `instFintypeSum` `Prod.pseudoEMetricSpaceMax` `EquivLike.toFunLike` `instEquivLike` `sumArrowIsometryEquivProdArrow`	—	—
`sumArrowIsometryEquivProdArrow_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `Prod.pseudoEMetricSpaceMax` `pseudoEMetricSpacePi` `instFintypeSum` `EquivLike.toFunLike` `instEquivLike` `symm` `sumArrowIsometryEquivProdArrow`	—	—
`sumArrowIsometryEquivProdArrow_toHomeomorph` 📖	mathematical	—	`toHomeomorph` `pseudoEMetricSpacePi` `instFintypeSum` `Prod.pseudoEMetricSpaceMax` `sumArrowIsometryEquivProdArrow` `Homeomorph.sumArrowHomeomorphProdArrow` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	—
`surjective` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `IsometryEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.left_inv`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `trans`	—	—
`toEquiv_inj` 📖	mathematical	—	`toEquiv`	—	`toEquiv_injective`
`toEquiv_injective` 📖	mathematical	—	`IsometryEquiv` `Equiv` `toEquiv`	—	—
`toEquiv_toHomeomorph` 📖	mathematical	—	`Homeomorph.toEquiv` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `toHomeomorph` `toEquiv`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—

IsometryEquiv.Simps

Definitions

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

MetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_induced` 📖	mathematical	—	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `toEMetricSpace` `induced`	—	—

PseudoEMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_induced` 📖	mathematical	—	`Isometry` `induced`	—	—

PseudoMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_induced` 📖	mathematical	—	`Isometry` `toPseudoEMetricSpace` `induced`	—	—

QuadraticMap

Definitions

Name	Category	Theorems
`Isometry` 📖	CompData	29 math math: `Isometry.ext_iff`, `Isometry.inl_apply`, `Isometry.single_apply`, `QuadraticModuleCat.forget₂_map_associator_inv`, `QuadraticModuleCat.forget₂_map`, `CategoryTheory.Iso.toIsometryEquiv_toFun`, `IsometryEquiv.toIsometry_apply`, `Isometry.snd_comp_inl`, `Isometry.snd_apply`, `CliffordAlgebra.map_apply_ι`, `Isometry.comp_apply`, `Isometry.map_app`, `QuadraticModuleCat.forget₂_map_associator_hom`, `Isometry.proj_comp_single_of_ne`, `QuadraticModuleCat.Hom.toIsometry_injective`, `QuadraticModuleCat.forget₂_obj`, `Isometry.instLinearMapClass`, `QuadraticForm.toDualProd_apply`, `Isometry.proj_apply`, `Isometry.fst_apply`, `Isometry.instSubsingleton`, `Isometry.fst_comp_inr`, `CategoryTheory.Iso.toIsometryEquiv_invFun`, `Isometry.inr_apply`, `Isometry.toLinearMap_injective`, `Isometry.tmul_apply`, `Isometry.id_apply`, `Isometry.ofEq_apply`, `Isometry.coe_toLinearMap`

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_isometry` 📖	mathematical	`Topology.IsEmbedding` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `Topology.IsInducing.comapPseudoMetricSpace` `toIsInducing`	—	`toIsInducing` `Isometry.of_dist_eq`

(root)

Definitions

Name	Category	Theorems
`Isometry` 📖	MathDef	101 math math: `Unitization.isometry_inr`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal`, `isometry_subsingleton`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `NumberField.InfinitePlace.isometry_embedding`, `GromovHausdorff.isometry_optimalGHInjr`, `Isometry.single`, `AddMonoidHomClass.isometry_of_norm`, `EMetric.NonemptyCompacts.isometry_toCloseds`, `ContinuousLinearMap.isometry_mul_flip`, `UniformOnFun.isometry_restrict`, `UpperHalfPlane.isometry_real_vadd`, `EMetric.Closeds.isometry_singleton`, `ContinuousMapZero.isometry_toContinuousMap`, `PseudoEMetricSpace.isometry_induced`, `UpperHalfPlane.isometry_vertical_line`, `TopologicalSpace.NonemptyCompacts.isometry_singleton`, `Complex.isometry_conj`, `WithAbs.isometry_of_comp`, `RegularNormedAlgebra.isometry_mul'`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbedding`, `star_isometry`, `UniformFun.isometry_ofFun_continuousMap`, `MulOpposite.isometry_opLinearEquiv`, `NormedAddGroupHom.isometry_id`, `PseudoMetricSpace.isometry_induced`, `WithLp.prod_isometry_ofLp_infty`, `isometry_cfcₙHom`, `Complex.isometry_ofReal`, `Isometry.of_dist_eq`, `isometry_mul_left`, `algebraMap_isometry`, `RingHom.isometry`, `TopologicalSpace.Closeds.isometry_singleton`, `BoundedContinuousFunction.isometry_extend`, `UniformFun.isometry_ofFun_boundedContinuousFunction`, `UniformSpace.Completion.coe_isometry`, `TopologicalSpace.Compacts.isometry_singleton`, `isometry_iff_dist_eq`, `MonoidHomClass.isometry_iff_norm`, `GromovHausdorff.ghDist_eq_hausdorffDist`, `SemiNormedGrp₁.iso_isometry`, `Isometry.of_nndist_eq`, `KuratowskiEmbedding.embeddingOfSubset_isometry`, `TopologicalSpace.NonemptyCompacts.isometry_toCloseds`, `EMetricSpace.isometry_induced`, `GromovHausdorff.AuxGluingStruct.isom`, `ContinuousLinearMap.isometry_mul`, `IsIsometricVAdd.isometry_vadd`, `Isometry.inl`, `LinearIsometry.isometry`, `AffineIsometry.isometry`, `NumberField.InfinitePlace.isometry_embedding_of_isReal`, `LinearIsometryEquiv.isometry`, `AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp`, `Metric.isometry_inl`, `IsometryEquiv.isometry_toFun`, `AddMonoidHomClass.isometry_iff_norm`, `ZeroAtInftyContinuousMap.isometry_toBCF`, `isometry_add_left`, `isometry_mul_right`, `NonUnitalStarAlgHom.isometry`, `IsIsometricSMul.isometry_smul`, `PiLp.isometry_ofLp_infty`, `Isometry.inr`, `MonoidHomClass.isometry_of_norm`, `EMetric.NonemptyCompacts.isometry_singleton`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal`, `Topology.IsEmbedding.to_isometry`, `lp.isometry_single`, `Metric.Sigma.isometry_mk`, `isometry_subtype_coe`, `isometry_add_right`, `gelfandTransform_isometry`, `MeasureTheory.isometry_lpMeasSubgroupToLpTrim`, `KuratowskiEmbedding.exists_isometric_embedding`, `isometry_neg`, `isometry_iff_nndist_eq`, `Metric.isometry_inr`, `IsometricContinuousFunctionalCalculus.isometric`, `SemiNormedGrp.iso_isometry_of_normNoninc`, `isometry_inv`, `IsometryClass.isometry`, `MetricSpace.isometry_induced`, `Metric.PiNatEmbed.isometry_embed`, `UpperHalfPlane.isometry_pos_mul`, `isometry_id`, `TopologicalSpace.Compacts.isometry_toCloseds`, `TopologicalSpace.NonemptyCompacts.isometry_toCompacts`, `AffineIsometryEquiv.isometry`, `GromovHausdorff.isometry_optimalGHInjl`, `WithLp.unitization_isometry_inr`, `GromovHausdorff.eq_toGHSpace_iff`, `SemilinearIsometryClass.isometry`, `IsUniformEmbedding.to_isometry`, `MeasureTheory.Lp.isometry_compMeasurePreserving`, `IsometryEquiv.isometry`, `StarAlgEquiv.isometry`, `Complex.isometry_intCast`, `kuratowskiEmbedding.isometry`, `isometry_cfcHom`
`IsometryClass` 📖	CompData	1 math math: `IsometryEquiv.instIsometryClass`
`«term_≃ᵢ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_id` 📖	mathematical	—	`Isometry`	—	—
`isometry_iff_dist_eq` 📖	mathematical	—	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	—
`isometry_iff_nndist_eq` 📖	mathematical	—	`Isometry` `PseudoMetricSpace.toPseudoEMetricSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`edist_nndist`
`isometry_subsingleton` 📖	mathematical	—	`Isometry`	—	`PseudoEMetricSpace.edist_self`
`isometry_subtype_coe` 📖	mathematical	—	`Isometry` `Set` `Set.instMembership` `instPseudoEMetricSpaceSubtype`	—	—

---

← Back to Index