IsometricSMul

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

Statistics

Metric	Count
Definitions `IsIsometricSMul`, `IsIsometricVAdd`, `addLeft`, `addRight`, `constSMul`, `constVAdd`, `divLeft`, `divRight`, `inv`, `mulLeft`, `mulRight`, `neg`, `subLeft`, `subRight`	14
Theorems `isIsometricVAdd`, `isIsIsometricVAdd`, `isIsIsometricVAdd'`, `isIsIsometricVAdd''`, `smul`, `vadd`, `preimage_add_left_ball`, `preimage_add_left_closedBall`, `preimage_add_right_ball`, `preimage_add_right_closedBall`, `preimage_mul_left_ball`, `preimage_mul_left_closedBall`, `preimage_mul_right_ball`, `preimage_mul_right_closedBall`, `preimage_smul_ball`, `preimage_smul_closedBall`, `preimage_vadd_ball`, `preimage_vadd_closedBall`, `smul_ball`, `smul_closedBall`, `vadd_ball`, `vadd_closedBall`, `isometry_smul`, `opposite_of_comm`, `to_continuousConstSMul`, `isometry_vadd`, `opposite_of_comm`, `to_continuousConstVAdd`, `addLeft_apply`, `addLeft_symm`, `addLeft_toEquiv`, `addRight_apply`, `addRight_symm`, `addRight_toEquiv`, `constSMul_apply`, `constSMul_symm`, `constSMul_toEquiv`, `constVAdd_apply`, `constVAdd_symm`, `constVAdd_toEquiv`, `divLeft_apply`, `divLeft_symm_apply`, `divLeft_toEquiv`, `divRight_apply`, `divRight_symm`, `divRight_toEquiv`, `inv_apply`, `inv_symm`, `inv_toEquiv`, `mulLeft_apply`, `mulLeft_symm`, `mulLeft_toEquiv`, `mulRight_apply`, `mulRight_symm`, `mulRight_toEquiv`, `neg_apply`, `neg_symm`, `neg_toEquiv`, `subLeft_apply`, `subLeft_symm_apply`, `subLeft_toEquiv`, `subRight_apply`, `subRight_symm`, `subRight_toEquiv`, `preimage_add_left_ball`, `preimage_add_left_closedBall`, `preimage_add_left_closedEBall`, `preimage_add_left_eball`, `preimage_add_right_ball`, `preimage_add_right_closedBall`, `preimage_add_right_closedEBall`, `preimage_add_right_eball`, `preimage_mul_left_ball`, `preimage_mul_left_closedBall`, `preimage_mul_left_closedEBall`, `preimage_mul_left_eball`, `preimage_mul_right_ball`, `preimage_mul_right_closedBall`, `preimage_mul_right_closedEBall`, `preimage_mul_right_eball`, `preimage_smul_ball`, `preimage_smul_closedBall`, `preimage_smul_closedEBall`, `preimage_smul_eball`, `preimage_smul_sphere`, `preimage_vadd_ball`, `preimage_vadd_closedBall`, `preimage_vadd_closedEBall`, `preimage_vadd_eball`, `preimage_vadd_sphere`, `smul_ball`, `smul_closedBall`, `smul_closedEBall`, `smul_eball`, `smul_sphere`, `vadd_ball`, `vadd_closedBall`, `vadd_closedEBall`, `vadd_eball`, `vadd_sphere`, `isIsIsometricVAdd''`, `isIsometricSMul`, `isIsometricSMul'`, `isIsometricSMul'`, `isIsometricSMul''`, `isIsometricVAdd'`, `isIsometricVAdd''`, `instIsIsometricSMul`, `instIsIsometricVAdd`, `isIsometricSMul'`, `isIsometricSMul''`, `isIsometricVAdd'`, `isIsometricVAdd''`, `isIsometricSMul`, `isIsometricSMul'`, `isIsometricVAdd`, `isIsometricVAdd'`, `isIsometricSMul`, `diam_smul`, `diam_vadd`, `dist_add_left`, `dist_add_right`, `dist_div_left`, `dist_div_right`, `dist_inv_inv`, `dist_mul_left`, `dist_mul_right`, `dist_neg_neg`, `dist_smul`, `dist_sub_left`, `dist_sub_right`, `dist_vadd`, `ediam_smul`, `ediam_vadd`, `edist_add_left`, `edist_add_right`, `edist_div_left`, `edist_div_right`, `edist_inv`, `edist_inv_inv`, `edist_mul_left`, `edist_mul_right`, `edist_neg`, `edist_neg_neg`, `edist_smul_left`, `edist_sub_left`, `edist_sub_right`, `edist_vadd_left`, `instIsIsometricSMulForall`, `instIsIsometricSMulMulOpposite`, `instIsIsometricVAddAddOpposite`, `instIsIsometricVAddForall`, `isometry_add_left`, `isometry_add_right`, `isometry_inv`, `isometry_mul_left`, `isometry_mul_right`, `isometry_neg`, `nndist_add_left`, `nndist_add_right`, `nndist_div_left`, `nndist_div_right`, `nndist_inv_inv`, `nndist_mul_left`, `nndist_mul_right`, `nndist_neg_neg`, `nndist_smul`, `nndist_sub_left`, `nndist_sub_right`, `nndist_vadd`	170
Total	184

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsometricVAdd` 📖	mathematical	—	`IsIsometricVAdd` `AddUnits` `instVAdd`	—	`IsIsometricVAdd.isometry_vadd`

Additive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsIsometricVAdd` 📖	mathematical	—	`IsIsometricVAdd` `Additive` `vadd`	—	`IsIsometricSMul.isometry_smul`
`isIsIsometricVAdd'` 📖	mathematical	—	`IsIsometricVAdd` `Additive` `instPseudoEMetricSpaceAdditive` `Add.toVAdd` `add`	—	`edist_smul_left`
`isIsIsometricVAdd''` 📖	mathematical	—	`IsIsometricVAdd` `AddOpposite` `Additive` `instPseudoEMetricSpaceAdditive` `Add.toVAddAddOpposite` `add`	—	`edist_smul_left`

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Set` `Set.smulSet`	—	`LipschitzWith.isBounded_image` `Isometry.lipschitz` `IsIsometricSMul.isometry_smul`
`vadd` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`LipschitzWith.isBounded_image` `Isometry.lipschitz` `IsIsometricVAdd.isometry_vadd`

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_add_left_ball` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Metric.eball` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Metric.preimage_add_left_eball`
`preimage_add_left_closedBall` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Metric.closedEBall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Metric.preimage_add_left_closedEBall`
`preimage_add_right_ball` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Metric.eball` `SubNegMonoid.toSub`	—	`Metric.preimage_add_right_eball`
`preimage_add_right_closedBall` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Metric.closedEBall` `SubNegMonoid.toSub`	—	`Metric.preimage_add_right_closedEBall`
`preimage_mul_left_ball` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Metric.eball` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Metric.preimage_mul_left_eball`
`preimage_mul_left_closedBall` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Metric.closedEBall` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Metric.preimage_mul_left_closedEBall`
`preimage_mul_right_ball` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Metric.eball` `DivInvMonoid.toDiv`	—	`Metric.preimage_mul_right_eball`
`preimage_mul_right_closedBall` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Metric.closedEBall` `DivInvMonoid.toDiv`	—	`Metric.preimage_mul_right_closedEBall`
`preimage_smul_ball` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Metric.eball` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Metric.preimage_smul_eball`
`preimage_smul_closedBall` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Metric.closedEBall` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Metric.preimage_smul_closedEBall`
`preimage_vadd_ball` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Metric.eball` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Metric.preimage_vadd_eball`
`preimage_vadd_closedBall` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Metric.closedEBall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Metric.preimage_vadd_closedEBall`
`smul_ball` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Metric.eball`	—	`Metric.smul_eball`
`smul_closedBall` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Metric.closedEBall`	—	`Metric.smul_closedEBall`
`vadd_ball` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Metric.eball`	—	`Metric.vadd_eball`
`vadd_closedBall` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Metric.closedEBall`	—	`Metric.vadd_closedEBall`

IsIsometricSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_smul` 📖	mathematical	—	`Isometry`	—	—
`opposite_of_comm` 📖	mathematical	—	`IsIsometricSMul` `MulOpposite`	—	`isometry_smul`
`to_continuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Isometry.continuous` `isometry_smul`

IsIsometricVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_vadd` 📖	mathematical	—	`Isometry` `HVAdd.hVAdd` `instHVAdd`	—	—
`opposite_of_comm` 📖	mathematical	—	`IsIsometricVAdd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd` `isometry_vadd`
`to_continuousConstVAdd` 📖	mathematical	—	`ContinuousConstVAdd` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Isometry.continuous` `isometry_vadd`

IsometryEquiv

Definitions

Name	Category	Theorems
`addLeft` 📖	CompOp	3 math math: `addLeft_symm`, `addLeft_apply`, `addLeft_toEquiv`
`addRight` 📖	CompOp	4 math math: `addRight_symm`, `subRight_symm`, `addRight_apply`, `addRight_toEquiv`
`constSMul` 📖	CompOp	3 math math: `constSMul_toEquiv`, `constSMul_symm`, `constSMul_apply`
`constVAdd` 📖	CompOp	3 math math: `constVAdd_toEquiv`, `constVAdd_symm`, `constVAdd_apply`
`divLeft` 📖	CompOp	3 math math: `divLeft_apply`, `divLeft_symm_apply`, `divLeft_toEquiv`
`divRight` 📖	CompOp	3 math math: `divRight_symm`, `divRight_apply`, `divRight_toEquiv`
`inv` 📖	CompOp	3 math math: `inv_toEquiv`, `inv_symm`, `inv_apply`
`mulLeft` 📖	CompOp	3 math math: `mulLeft_apply`, `mulLeft_symm`, `mulLeft_toEquiv`
`mulRight` 📖	CompOp	4 math math: `divRight_symm`, `mulRight_toEquiv`, `mulRight_symm`, `mulRight_apply`
`neg` 📖	CompOp	3 math math: `neg_toEquiv`, `neg_apply`, `neg_symm`
`subLeft` 📖	CompOp	3 math math: `subLeft_symm_apply`, `subLeft_toEquiv`, `subLeft_apply`
`subRight` 📖	CompOp	3 math math: `subRight_apply`, `subRight_symm`, `subRight_toEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `addLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`addLeft_symm` 📖	mathematical	—	`symm` `addLeft` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`constVAdd_symm`
`addLeft_toEquiv` 📖	mathematical	—	`toEquiv` `addLeft` `Equiv.addLeft`	—	—
`addRight_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `addRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`addRight_symm` 📖	mathematical	—	`symm` `addRight` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext`
`addRight_toEquiv` 📖	mathematical	—	`toEquiv` `addRight` `Equiv.addRight`	—	—
`constSMul_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `constSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`constSMul_symm` 📖	mathematical	—	`symm` `constSMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext`
`constSMul_toEquiv` 📖	mathematical	—	`toEquiv` `constSMul` `MulAction.toPerm`	—	—
`constVAdd_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `constVAdd` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`constVAdd_symm` 📖	mathematical	—	`symm` `constVAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext`
`constVAdd_toEquiv` 📖	mathematical	—	`toEquiv` `constVAdd` `AddAction.toPerm`	—	—
`divLeft_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `divLeft` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`divLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `divLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`divLeft_toEquiv` 📖	mathematical	—	`toEquiv` `divLeft` `Equiv.divLeft`	—	—
`divRight_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `divRight` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`divRight_symm` 📖	mathematical	—	`symm` `divRight` `mulRight`	—	`ext`
`divRight_toEquiv` 📖	mathematical	—	`toEquiv` `divRight` `Equiv.divRight`	—	—
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `inv` `InvolutiveInv.toInv` `DivisionMonoid.toInvolutiveInv` `Group.toDivisionMonoid`	—	—
`inv_symm` 📖	mathematical	—	`symm` `inv`	—	—
`inv_toEquiv` 📖	mathematical	—	`toEquiv` `inv` `Equiv.inv` `DivisionMonoid.toInvolutiveInv` `Group.toDivisionMonoid`	—	—
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mulLeft_symm` 📖	mathematical	—	`symm` `mulLeft` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`constSMul_symm`
`mulLeft_toEquiv` 📖	mathematical	—	`toEquiv` `mulLeft` `Equiv.mulLeft`	—	—
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mulRight_symm` 📖	mathematical	—	`symm` `mulRight` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext`
`mulRight_toEquiv` 📖	mathematical	—	`toEquiv` `mulRight` `Equiv.mulRight`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `neg` `InvolutiveNeg.toNeg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid`	—	—
`neg_symm` 📖	mathematical	—	`symm` `neg`	—	—
`neg_toEquiv` 📖	mathematical	—	`toEquiv` `neg` `Equiv.neg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid`	—	—
`subLeft_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `subLeft` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`subLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `subLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`subLeft_toEquiv` 📖	mathematical	—	`toEquiv` `subLeft` `Equiv.subLeft`	—	—
`subRight_apply` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EquivLike.toFunLike` `instEquivLike` `subRight` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`subRight_symm` 📖	mathematical	—	`symm` `subRight` `addRight`	—	`ext`
`subRight_toEquiv` 📖	mathematical	—	`toEquiv` `subRight` `Equiv.subRight`	—	—

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_add_left_ball` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ball` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`preimage_vadd_ball`
`preimage_add_left_closedBall` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closedBall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`preimage_vadd_closedBall`
`preimage_add_left_closedEBall` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closedEBall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`preimage_vadd_closedEBall`
`preimage_add_left_eball` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `eball` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`preimage_vadd_eball`
`preimage_add_right_ball` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ball` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `preimage_vadd_ball`
`preimage_add_right_closedBall` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closedBall` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `preimage_vadd_closedBall`
`preimage_add_right_closedEBall` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `closedEBall` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `preimage_vadd_closedEBall`
`preimage_add_right_eball` 📖	mathematical	—	`Set.preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `eball` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `preimage_vadd_eball`
`preimage_mul_left_ball` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ball` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`preimage_smul_ball`
`preimage_mul_left_closedBall` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closedBall` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`preimage_smul_closedBall`
`preimage_mul_left_closedEBall` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closedEBall` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`preimage_smul_closedEBall`
`preimage_mul_left_eball` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `eball` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`preimage_smul_eball`
`preimage_mul_right_ball` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ball` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `preimage_smul_ball`
`preimage_mul_right_closedBall` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closedBall` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `preimage_smul_closedBall`
`preimage_mul_right_closedEBall` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `closedEBall` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `preimage_smul_closedEBall`
`preimage_mul_right_eball` 📖	mathematical	—	`Set.preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `eball` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `preimage_smul_eball`
`preimage_smul_ball` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `ball` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.preimage_smul` `smul_ball`
`preimage_smul_closedBall` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `closedBall` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.preimage_smul` `smul_closedBall`
`preimage_smul_closedEBall` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `closedEBall` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.preimage_smul` `smul_closedEBall`
`preimage_smul_eball` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `eball` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.preimage_smul` `smul_eball`
`preimage_smul_sphere` 📖	mathematical	—	`Set.preimage` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `sphere` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.preimage_smul` `smul_sphere`
`preimage_vadd_ball` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `ball` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.preimage_vadd` `vadd_ball`
`preimage_vadd_closedBall` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `closedBall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.preimage_vadd` `vadd_closedBall`
`preimage_vadd_closedEBall` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `closedEBall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.preimage_vadd` `vadd_closedEBall`
`preimage_vadd_eball` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `eball` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.preimage_vadd` `vadd_eball`
`preimage_vadd_sphere` 📖	mathematical	—	`Set.preimage` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `sphere` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.preimage_vadd` `vadd_sphere`
`smul_ball` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `ball`	—	`IsometryEquiv.image_ball`
`smul_closedBall` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `closedBall`	—	`IsometryEquiv.image_closedBall`
`smul_closedEBall` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `closedEBall`	—	`IsometryEquiv.image_closedEBall`
`smul_eball` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `eball`	—	`IsometryEquiv.image_eball`
`smul_sphere` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `sphere`	—	`IsometryEquiv.image_sphere`
`vadd_ball` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `ball`	—	`IsometryEquiv.image_ball`
`vadd_closedBall` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `closedBall`	—	`IsometryEquiv.image_closedBall`
`vadd_closedEBall` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `closedEBall`	—	`IsometryEquiv.image_closedEBall`
`vadd_eball` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `eball`	—	`IsometryEquiv.image_eball`
`vadd_sphere` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `sphere`	—	`IsometryEquiv.image_sphere`

Multiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsIsometricVAdd''` 📖	mathematical	—	`IsIsometricSMul` `MulOpposite` `Multiplicative` `instPseudoEMetricSpaceMultiplicative` `Mul.toSMulMulOpposite` `mul`	—	`edist_vadd_left`
`isIsometricSMul` 📖	mathematical	—	`IsIsometricSMul` `Multiplicative` `smul`	—	`IsIsometricVAdd.isometry_vadd`
`isIsometricSMul'` 📖	mathematical	—	`IsIsometricSMul` `Multiplicative` `instPseudoEMetricSpaceMultiplicative` `mul`	—	`edist_vadd_left`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsometricSMul'` 📖	mathematical	`IsIsometricSMul`	`pseudoEMetricSpacePi` `smul'`	—	`Isometry.piMap` `IsIsometricSMul.isometry_smul`
`isIsometricSMul''` 📖	mathematical	`IsIsometricSMul` `MulOpposite` `Mul.toSMulMulOpposite`	`pseudoEMetricSpacePi` `instMul`	—	`Isometry.piMap` `isometry_mul_right`
`isIsometricVAdd'` 📖	mathematical	`IsIsometricVAdd`	`pseudoEMetricSpacePi` `vadd'`	—	`Isometry.piMap` `IsIsometricVAdd.isometry_vadd`
`isIsometricVAdd''` 📖	mathematical	`IsIsometricVAdd` `AddOpposite` `Add.toVAddAddOpposite`	`pseudoEMetricSpacePi` `instAdd`	—	`Isometry.piMap` `isometry_add_right`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsometricSMul` 📖	mathematical	—	`IsIsometricSMul` `pseudoEMetricSpaceMax` `instSMul`	—	`Isometry.prodMap` `IsIsometricSMul.isometry_smul`
`instIsIsometricVAdd` 📖	mathematical	—	`IsIsometricVAdd` `pseudoEMetricSpaceMax` `instVAdd`	—	`Isometry.prodMap` `IsIsometricVAdd.isometry_vadd`
`isIsometricSMul'` 📖	mathematical	—	`IsIsometricSMul` `pseudoEMetricSpaceMax` `instMul`	—	`Isometry.prodMap` `IsIsometricSMul.isometry_smul`
`isIsometricSMul''` 📖	mathematical	—	`IsIsometricSMul` `MulOpposite` `pseudoEMetricSpaceMax` `Mul.toSMulMulOpposite` `instMul`	—	`Isometry.prodMap` `isometry_mul_right`
`isIsometricVAdd'` 📖	mathematical	—	`IsIsometricVAdd` `pseudoEMetricSpaceMax` `Add.toVAdd` `instAdd`	—	`Isometry.prodMap` `IsIsometricVAdd.isometry_vadd`
`isIsometricVAdd''` 📖	mathematical	—	`IsIsometricVAdd` `AddOpposite` `pseudoEMetricSpaceMax` `Add.toVAddAddOpposite` `instAdd`	—	`Isometry.prodMap` `isometry_add_right`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsometricSMul` 📖	mathematical	—	`IsIsometricSMul` `smulLeft`	—	`IsIsometricSMul.isometry_smul`
`isIsometricSMul'` 📖	mathematical	—	`IsIsometricSMul` `instPseudoEMetricSpaceULift` `smul`	—	`edist_smul_left`
`isIsometricVAdd` 📖	mathematical	—	`IsIsometricVAdd` `vaddLeft`	—	`IsIsometricVAdd.isometry_vadd`
`isIsometricVAdd'` 📖	mathematical	—	`IsIsometricVAdd` `instPseudoEMetricSpaceULift` `vadd`	—	`edist_vadd_left`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsometricSMul` 📖	mathematical	—	`IsIsometricSMul` `Units` `instSMul`	—	`IsIsometricSMul.isometry_smul`

(root)

Definitions

Name	Category	Theorems
`IsIsometricSMul` 📖	CompData	15 math math: `NormedGroup.to_isIsometricSMul_right`, `Multiplicative.isIsIsometricVAdd''`, `ULift.isIsometricSMul'`, `Units.isIsometricSMul`, `ULift.isIsometricSMul`, `IsIsometricSMul.opposite_of_comm`, `Prod.instIsIsometricSMul`, `Prod.isIsometricSMul''`, `UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal`, `Multiplicative.isIsometricSMul'`, `DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp`, `instIsIsometricSMulMulOpposite`, `NormedGroup.to_isIsometricSMul_left`, `Prod.isIsometricSMul'`, `Multiplicative.isIsometricSMul`
`IsIsometricVAdd` 📖	CompData	15 math math: `Prod.isIsometricVAdd''`, `DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp`, `Additive.isIsIsometricVAdd`, `instIsIsometricVAddAddOpposite`, `ULift.isIsometricVAdd`, `Additive.isIsIsometricVAdd'`, `IsIsometricVAdd.opposite_of_comm`, `NormedAddGroup.to_isIsometricVAdd_left`, `NormedAddGroup.to_isIsometricVAdd_right`, `AddUnits.isIsometricVAdd`, `NormedAddTorsor.to_isIsIsometricVAdd`, `ULift.isIsometricVAdd'`, `Additive.isIsIsometricVAdd''`, `Prod.instIsIsometricVAdd`, `Prod.isIsometricVAdd'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diam_smul` 📖	mathematical	—	`Metric.diam` `Set` `Set.smulSet`	—	`Isometry.diam_image` `IsIsometricSMul.isometry_smul`
`diam_vadd` 📖	mathematical	—	`Metric.diam` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`Isometry.diam_image` `IsIsometricVAdd.isometry_vadd`
`dist_add_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_vadd`
`dist_add_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_vadd`
`dist_div_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `dist_mul_left` `dist_inv_inv`
`dist_div_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `dist_mul_right`
`dist_inv_inv` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`IsometryEquiv.dist_eq`
`dist_mul_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_smul`
`dist_mul_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_smul`
`dist_neg_neg` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`IsometryEquiv.dist_eq`
`dist_smul` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist`	—	`Isometry.dist_eq` `IsIsometricSMul.isometry_smul`
`dist_sub_left` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `dist_add_left` `dist_neg_neg`
`dist_sub_right` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `dist_add_right`
`dist_vadd` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `HVAdd.hVAdd` `instHVAdd`	—	`Isometry.dist_eq` `IsIsometricVAdd.isometry_vadd`
`ediam_smul` 📖	mathematical	—	`Metric.ediam` `Set` `Set.smulSet`	—	`Isometry.ediam_image` `IsIsometricSMul.isometry_smul`
`ediam_vadd` 📖	mathematical	—	`Metric.ediam` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`Isometry.ediam_image` `IsIsometricVAdd.isometry_vadd`
`edist_add_left` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`isometry_add_left`
`edist_add_right` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`isometry_add_right`
`edist_div_left` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `edist_mul_left` `edist_inv_inv`
`edist_div_right` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `edist_mul_right`
`edist_inv` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`edist_inv_inv` `inv_inv`
`edist_inv_inv` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`edist_mul_left` `edist_mul_right` `mul_inv_cancel` `one_mul` `inv_mul_cancel_right` `PseudoEMetricSpace.edist_comm`
`edist_mul_left` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`isometry_mul_left`
`edist_mul_right` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`isometry_mul_right`
`edist_neg` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`edist_neg_neg` `neg_neg`
`edist_neg_neg` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`edist_add_left` `edist_add_right` `add_neg_cancel` `zero_add` `neg_add_cancel_right` `PseudoEMetricSpace.edist_comm`
`edist_smul_left` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist`	—	`IsIsometricSMul.isometry_smul`
`edist_sub_left` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `edist_add_left` `edist_neg_neg`
`edist_sub_right` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `edist_add_right`
`edist_vadd_left` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `HVAdd.hVAdd` `instHVAdd`	—	`IsIsometricVAdd.isometry_vadd`
`instIsIsometricSMulForall` 📖	mathematical	`IsIsometricSMul`	`pseudoEMetricSpacePi` `Pi.instSMul`	—	`Isometry.piMap` `IsIsometricSMul.isometry_smul`
`instIsIsometricSMulMulOpposite` 📖	mathematical	—	`IsIsometricSMul` `MulOpposite` `MulOpposite.instPseudoEMetricSpace` `MulOpposite.instSMul`	—	`edist_smul_left`
`instIsIsometricVAddAddOpposite` 📖	mathematical	—	`IsIsometricVAdd` `AddOpposite` `AddOpposite.instPseudoEMetricSpace` `AddOpposite.instVAdd`	—	`edist_vadd_left`
`instIsIsometricVAddForall` 📖	mathematical	`IsIsometricVAdd`	`pseudoEMetricSpacePi` `Pi.instVAdd`	—	`Isometry.piMap` `IsIsometricVAdd.isometry_vadd`
`isometry_add_left` 📖	mathematical	—	`Isometry`	—	`IsIsometricVAdd.isometry_vadd`
`isometry_add_right` 📖	mathematical	—	`Isometry`	—	`IsIsometricVAdd.isometry_vadd`
`isometry_inv` 📖	mathematical	—	`Isometry` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`edist_inv_inv`
`isometry_mul_left` 📖	mathematical	—	`Isometry`	—	`IsIsometricSMul.isometry_smul`
`isometry_mul_right` 📖	mathematical	—	`Isometry`	—	`IsIsometricSMul.isometry_smul`
`isometry_neg` 📖	mathematical	—	`Isometry` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`edist_neg_neg`
`nndist_add_left` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`nndist_vadd`
`nndist_add_right` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`nndist_vadd`
`nndist_div_left` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `nndist_mul_left` `nndist_inv_inv`
`nndist_div_right` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `nndist_mul_right`
`nndist_inv_inv` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`IsometryEquiv.nndist_eq`
`nndist_mul_left` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`nndist_smul`
`nndist_mul_right` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`nndist_smul`
`nndist_neg_neg` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`IsometryEquiv.nndist_eq`
`nndist_smul` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`Isometry.nndist_eq` `IsIsometricSMul.isometry_smul`
`nndist_sub_left` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `nndist_add_left` `nndist_neg_neg`
`nndist_sub_right` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `nndist_add_right`
`nndist_vadd` 📖	mathematical	—	`NNDist.nndist` `PseudoMetricSpace.toNNDist` `HVAdd.hVAdd` `instHVAdd`	—	`Isometry.nndist_eq` `IsIsometricVAdd.isometry_vadd`

---

← Back to Index