SignedDist

📁 Source: Mathlib/Geometry/Euclidean/SignedDist.lean

Statistics

Metric	Count
Definitions `signedInfDist`, `signedInfDist`, `signedDist`	3
Theorems `abs_signedInfDist_eq_dist_of_mem_affineSpan_range`, `signedInfDist_affineCombination`, `signedInfDist_apply_of_ne`, `signedInfDist_apply_self`, `signedInfDist_reindex`, `abs_signedInfDist_eq_dist_of_mem_affineSpan_insert`, `signedInfDist_apply_of_mem`, `signedInfDist_apply_self`, `signedInfDist_def`, `signedInfDist_eq_const_of_mem`, `signedInfDist_eq_signedDist_of_mem`, `signedInfDist_eq_signedDist_orthogonalProjection`, `signedInfDist_singleton`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `abs_signedDist_le_dist`, `signedDist_anticomm`, `signedDist_apply`, `signedDist_apply_apply`, `signedDist_apply_linear`, `signedDist_apply_linear_apply`, `signedDist_congr`, `signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_eq_zero_of_orthogonal`, `signedDist_le_dist`, `signedDist_left_congr`, `signedDist_left_lineMap`, `signedDist_lineMap_left`, `signedDist_lineMap_lineMap`, `signedDist_lineMap_right`, `signedDist_linear_apply`, `signedDist_linear_apply_apply`, `signedDist_neg`, `signedDist_right_congr`, `signedDist_right_lineMap`, `signedDist_self`, `signedDist_smul`, `signedDist_smul_of_neg`, `signedDist_smul_of_pos`, `signedDist_triangle`, `signedDist_triangle_left`, `signedDist_triangle_right`, `signedDist_vadd_left`, `signedDist_vadd_left_swap`, `signedDist_vadd_right`, `signedDist_vadd_right_swap`, `signedDist_vadd_vadd`, `signedDist_vsub_self`, `signedDist_vsub_self_rev`, `signedDist_zero`	49
Total	52

Affine.Simplex

Definitions

Name	Category	Theorems
`signedInfDist` 📖	CompOp	16 math math: `sign_signedInfDist_lineMap_incenter_touchpoint`, `ExcenterExists.sign_signedInfDist_touchpoint`, `signedInfDist_apply_self`, `ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint`, `exists_forall_signedInfDist_eq_iff_eq_incenter`, `sign_signedInfDist_touchpoint_empty`, `signedInfDist_reindex`, `abs_signedInfDist_eq_dist_of_mem_affineSpan_range`, `ExcenterExists.signedInfDist_excenter`, `sign_signedInfDist_incenter`, `ExcenterExists.sign_signedInfDist_excenter`, `signedInfDist_affineCombination`, `ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv`, `exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter`, `signedInfDist_apply_of_ne`, `signedInfDist_incenter`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_signedInfDist_eq_dist_of_mem_affineSpan_range` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `points`	`abs` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `ContinuousAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `Dist.dist` `PseudoMetricSpace.toDist` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `faceOpposite` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `AffineSubspace.toAddTorsor` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `orthogonalProjectionSpan`	—	`instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `signedInfDist.eq_1` `AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert` `affineSpan_insert_affineSpan` `Set.insert_image_compl_eq_range` `orthogonalProjectionSpan.eq_1` `range_faceOpposite_points` `EuclideanGeometry.orthogonalProjection_congr`
`signedInfDist_affineCombination` 📖	mathematical	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Fin.fintype` `Real.instOne`	`DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `points` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AffineSubspace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `faceOpposite` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `AffineSubspace.toAddTorsor` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `orthogonalProjectionSpan`	—	`instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `ContinuousAffineMap.coe_toAffineMap` `Finset.map_affineCombination` `Finset.affineCombination_apply_eq_lineMap_sum` `Finset.inter_singleton_of_mem` `signedInfDist_apply_self` `signedInfDist_apply_of_ne` `Finset.sum_congr` `Finset.sum_singleton` `sub_zero` `add_zero`
`signedInfDist_apply_of_ne` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `points` `Real.instZero`	—	`AffineSubspace.signedInfDist_apply_of_mem` `mem_affineSpan_image_iff` `Real.instNontrivial`
`signedInfDist_apply_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `points` `Norm.norm` `NormedAddCommGroup.toNorm` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AffineSubspace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.range` `faceOpposite` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `AffineSubspace.toAddTorsor` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `orthogonalProjectionSpan`	—	`instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.instNonemptyRange` `AffineSubspace.signedInfDist_apply_self` `range_faceOpposite_points` `EuclideanGeometry.orthogonalProjection_congr`
`signedInfDist_reindex` 📖	mathematical	—	`signedInfDist` `reindex` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Set.image_congr` `AffineSubspace.signedInfDist.congr_simp` `Set.image_comp` `Set.image_compl_eq` `Equiv.bijective` `Set.image_singleton`

AffineSubspace

Definitions

Name	Category	Theorems
`signedInfDist` 📖	CompOp	8 math math: `signedInfDist_eq_signedDist_of_mem`, `signedInfDist_eq_signedDist_orthogonalProjection`, `abs_signedInfDist_eq_dist_of_mem_affineSpan_insert`, `signedInfDist_eq_const_of_mem`, `signedInfDist_singleton`, `signedInfDist_def`, `signedInfDist_apply_self`, `signedInfDist_apply_of_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_signedInfDist_eq_dist_of_mem_affineSpan_insert` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `instSetLike` `affineSpan` `Set` `Set.instInsert` `SetLike.coe`	`abs` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `ContinuousAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `Dist.dist` `PseudoMetricSpace.toDist` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `toAddTorsor` `EuclideanGeometry.orthogonalProjection`	—	`mem_affineSpan_insert_iff` `instIsTopologicalAddTorsor_1` `ContinuousAffineMap.map_vadd` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `ContinuousAffineMap.contLinear_map_vsub` `signedInfDist_apply_self` `signedInfDist_apply_of_mem` `sub_zero` `add_zero` `abs_mul` `Real.instIsOrderedRing` `abs_norm` `instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection` `IsScalarTower.left` `EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection` `smul_zero` `zero_vadd` `EuclideanGeometry.orthogonalProjection_eq_self_iff` `dist_eq_norm_vsub` `vadd_vsub` `norm_smul` `NormedSpace.toNormSMulClass`
`signedInfDist_apply_of_mem` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `instSetLike`	`DFunLike.coe` `ContinuousAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `Real.instZero`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedInfDist_eq_signedDist_orthogonalProjection` `EuclideanGeometry.orthogonalProjection_eq_self_iff` `signedDist_self`
`signedInfDist_apply_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `Norm.norm` `NormedAddCommGroup.toNorm` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AffineSubspace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SetLike.instMembership` `instSetLike` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `toAddTorsor` `EuclideanGeometry.orthogonalProjection`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedInfDist_eq_signedDist_orthogonalProjection` `signedDist_vsub_self` `dist_eq_norm_vsub'`
`signedInfDist_def` 📖	mathematical	—	`signedInfDist` `DFunLike.coe` `AffineMap` `Real` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AffineSubspace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SetLike.instMembership` `instSetLike` `Submodule` `Submodule.setLike` `direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `toAddTorsor` `ContinuousAffineMap.instFunLike` `EuclideanGeometry.orthogonalProjection`	—	—
`signedInfDist_eq_const_of_mem` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `instSetLike`	`ContinuousAffineMap.toAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `signedInfDist` `AffineMap.const` `Real.instZero`	—	`AffineMap.ext` `instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `EuclideanGeometry.orthogonalProjection_eq_self_iff` `vsub_self` `signedDist_zero`
`signedInfDist_eq_signedDist_of_mem` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SetLike.instMembership` `instSetLike`	`signedInfDist` `DFunLike.coe` `AffineMap` `ContinuousAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Submodule` `Submodule.setLike` `direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `toAddTorsor` `ContinuousAffineMap.instFunLike` `EuclideanGeometry.orthogonalProjection`	—	`signedDist_left_congr` `Submodule.inner_left_of_mem_orthogonal` `vsub_mem_direction` `SetLike.coe_mem` `EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal`
`signedInfDist_eq_signedDist_orthogonalProjection` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `signedInfDist` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AffineSubspace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SetLike.instMembership` `instSetLike` `Submodule` `Submodule.setLike` `direction` `Submodule.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.module` `instTopologicalSpaceSubtype` `toAddTorsor` `EuclideanGeometry.orthogonalProjection`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedInfDist_eq_signedDist_of_mem` `EuclideanGeometry.orthogonalProjection_mem`
`signedInfDist_singleton` 📖	mathematical	—	`signedInfDist` `affineSpan` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instSingletonSet` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Set.Elem` `Unique.instInhabited` `Set.uniqueSingleton` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `direction` `complete_of_proper` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `finiteDimensional_direction_affineSpan_singleton` `Real.instDivisionRing` `DFunLike.coe` `AffineMap` `ContinuousAffineMap` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `finiteDimensional_direction_affineSpan_singleton` `instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `EuclideanGeometry.orthogonalProjection_affineSpan_singleton` `signedInfDist_eq_signedDist_of_mem` `mem_affineSpan` `Set.mem_singleton`

(root)

Definitions

Name	Category	Theorems
`signedDist` 📖	CompOp	40 math math: `signedDist_right_congr`, `signedDist_left_congr`, `signedDist_triangle`, `signedDist_linear_apply_apply`, `signedDist_le_dist`, `signedDist_apply_apply`, `signedDist_eq_zero_of_orthogonal`, `signedDist_congr`, `AffineSubspace.signedInfDist_eq_signedDist_of_mem`, `signedDist_zero`, `AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection`, `signedDist_triangle_left`, `signedDist_smul_of_pos`, `signedDist_lineMap_lineMap`, `signedDist_vadd_left_swap`, `signedDist_vadd_right`, `signedDist_lineMap_left`, `signedDist_anticomm`, `signedDist_triangle_right`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_neg`, `signedDist_vsub_self_rev`, `signedDist_linear_apply`, `signedDist_self`, `signedDist_vsub_self`, `signedDist_smul`, `signedDist_smul_of_neg`, `signedDist_vadd_right_swap`, `signedDist_vadd_left`, `signedDist_apply_linear_apply`, `AffineSubspace.signedInfDist_singleton`, `signedDist_right_lineMap`, `AffineSubspace.signedInfDist_def`, `signedDist_lineMap_right`, `signedDist_apply`, `signedDist_eq_dist_iff_vsub_mem_span`, `abs_signedDist_le_dist`, `signedDist_apply_linear`, `signedDist_left_lineMap`, `signedDist_vadd_vadd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_signedDist_eq_dist_iff_vsub_mem_span` 📖	mathematical	—	`abs` `Real` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Dist.dist` `PseudoMetricSpace.toDist` `Submodule` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `Submodule.mem_span_singleton` `signedDist_apply_apply` `dist_eq_norm_vsub'` `NormedSpace.normalize.eq_1` `real_inner_smul_left` `abs_mul` `Real.instIsOrderedRing` `abs_inv` `Real.instIsStrictOrderedRing` `abs_norm` `norm_zero` `inv_zero` `inner_zero_left` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MulZeroClass.mul_zero` `smul_zero` `inv_mul_eq_iff_eq_mul₀` `ne_of_gt` `norm_pos_iff` `Real.norm_eq_abs` `List.TFAE.out` `norm_inner_eq_norm_tfae`
`abs_signedDist_le_dist` 📖	mathematical	—	`Real` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_apply_apply` `NormedSpace.normalize_zero_eq_zero` `inner_zero_left` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_imp_le_of_le_of_le` `abs_real_inner_le_norm` `le_refl` `NormedSpace.norm_normalize` `one_mul` `dist_eq_norm_vsub'`
`signedDist_anticomm` 📖	mathematical	—	`Real` `Real.instNeg` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `neg_vsub_eq_vsub_rev`
`signedDist_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Real` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `ContinuousAffineMap.comp` `SeminormedAddCommGroup.toAddCommGroup` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedField.toNormedCommRing` `RCLike.innerProductSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toContinuousAffineMap` `ContinuousLinearMap` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `starRingEnd` `RCLike.toStarRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `AddCommMonoid.toAddMonoid` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `ContinuousLinearMap.funLike` `innerSL` `NormedSpace.normalize` `VSub.vsub` `AddTorsor.toVSub` `ContinuousAffineMap.id` `ContinuousAffineMap.const`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1`
`signedDist_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Inner.inner` `InnerProductSpace.toInner` `NormedSpace.normalize` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1`
`signedDist_apply_linear` 📖	mathematical	—	`AffineMap.linear` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.toAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DFunLike.coe` `AffineMap` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toAddCommGroup` `Real.instAddCommMonoid` `NormedField.toNormedSpace` `LinearMap.addCommMonoid` `LinearMap.module` `LinearMap.instFunLike` `innerₗ` `NormedSpace.normalize`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `RingHomCompTriple.ids` `LinearMap.comp.congr_simp` `sub_zero`
`signedDist_apply_linear_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Ring.toSemiring` `Real.instRing` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `AffineMap.linear` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.toAffineMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AffineMap` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Inner.inner` `InnerProductSpace.toInner` `NormedSpace.normalize`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_apply_linear`
`signedDist_congr` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike`	`signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `AffineMap.ext` `ContinuousAffineMap.ext` `sign_pos` `one_mul` `signedDist_smul`
`signedDist_eq_dist_iff_vsub_mem_span` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Dist.dist` `PseudoMetricSpace.toDist` `Submodule` `NNReal` `instSemiringNNReal` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NNReal.instModuleOfReal` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `Submodule.mem_span_singleton` `signedDist_apply_apply` `dist_eq_norm_vsub'` `NormedSpace.normalize.eq_1` `real_inner_smul_left` `norm_zero` `inv_zero` `inner_zero_left` `MulZeroClass.mul_zero` `smul_zero` `inv_mul_eq_iff_eq_mul₀` `ne_of_gt` `norm_pos_iff` `inner_eq_norm_mul_iff_real` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `smul_smul` `inv_mul_cancel₀` `one_smul` `norm_smul` `NormedSpace.toNormSMulClass` `mul_comm` `NNReal.abs_eq`
`signedDist_eq_zero_of_orthogonal` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Real.instZero`	`DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_self` `signedDist_right_congr`
`signedDist_le_dist` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Dist.dist` `PseudoMetricSpace.toDist`	—	`le_trans` `instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `le_abs_self` `abs_signedDist_le_dist`
`signedDist_left_congr` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Real.instZero`	`DFunLike.coe` `AffineMap` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`ContinuousAffineMap.ext` `instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `vsub_vadd` `real_inner_smul_left` `MulZeroClass.mul_zero` `neg_zero` `zero_add` `signedDist_vadd_left`
`signedDist_left_lineMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Ring.toAddCommGroup` `Semiring.toModule` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.lineMap` `Real.instMul`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `ContinuousAffineMap.apply_lineMap` `signedDist_self` `AffineMap.lineMap_apply_zero` `sub_zero` `signedDist_lineMap_lineMap`
`signedDist_lineMap_left` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Ring.toAddCommGroup` `Semiring.toModule` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.lineMap` `Real.instMul` `Real.instNeg`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `AffineMap.apply_lineMap` `ContinuousAffineMap.lineMap_apply'` `signedDist_self` `neg_mul` `AffineMap.lineMap_apply_zero` `zero_sub` `signedDist_lineMap_lineMap`
`signedDist_lineMap_lineMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Ring.toAddCommGroup` `Semiring.toModule` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.lineMap` `Real.instMul` `Real.instSub`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `AffineMap.apply_lineMap` `ContinuousAffineMap.apply_lineMap` `ContinuousAffineMap.lineMap_apply'` `signedDist_self` `sub_zero` `add_zero` `zero_sub` `signedDist_anticomm` `add_sub_cancel_left` `sub_mul` `mul_neg` `sub_eq_add_neg`
`signedDist_lineMap_right` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Ring.toAddCommGroup` `Semiring.toModule` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.lineMap` `Real.instMul` `Real.instSub` `Real.instOne`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `AffineMap.apply_lineMap` `ContinuousAffineMap.lineMap_apply'` `signedDist_self` `AffineMap.lineMap_apply_one` `signedDist_lineMap_lineMap`
`signedDist_linear_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Ring.toSemiring` `Real.instRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousAffineMap` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AddCommGroup.toAddCommMonoid` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `LinearMap.instFunLike` `AffineMap.linear` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `signedDist` `ContinuousAffineMap.const` `Inner.inner` `InnerProductSpace.toInner` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.normalize`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1`
`signedDist_linear_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instFunLike` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `LinearMap.instFunLike` `AffineMap.linear` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `signedDist` `Inner.inner` `InnerProductSpace.toInner` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.normalize`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1`
`signedDist_neg` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real.instNeg`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `neg_smul` `one_smul` `sign_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `SignType.coe_neg` `neg_mul` `one_mul` `signedDist_smul`
`signedDist_right_congr` 📖	mathematical	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `Real.instZero`	`DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `vsub_vadd` `real_inner_smul_left` `MulZeroClass.mul_zero` `zero_add` `signedDist_vadd_right`
`signedDist_right_lineMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Ring.toAddCommGroup` `Semiring.toModule` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.lineMap` `Real.instMul` `Real.instSub` `Real.instOne`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `ContinuousAffineMap.apply_lineMap` `signedDist_self` `AffineMap.lineMap_apply_one` `signedDist_lineMap_lineMap`
`signedDist_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `Real.instZero`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `vsub_self` `inner_zero_right`
`signedDist_smul` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Real.instMul` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `NormedSpace.normalize_smul` `real_inner_smul_left`
`signedDist_smul_of_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Real.instNeg`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_smul` `sign_neg` `SignType.coe_neg` `neg_mul` `one_mul`
`signedDist_smul_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_smul` `sign_pos` `one_mul`
`signedDist_triangle` 📖	mathematical	—	`Real` `Real.instAdd` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `add_comm` `inner_add_right` `vsub_add_vsub_cancel`
`signedDist_triangle_left` 📖	mathematical	—	`Real` `Real.instSub` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `sub_eq_iff_eq_add'` `signedDist_triangle`
`signedDist_triangle_right` 📖	mathematical	—	`Real` `Real.instSub` `DFunLike.coe` `ContinuousAffineMap` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `sub_eq_iff_eq_add` `signedDist_triangle`
`signedDist_vadd_left` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instAdd` `Real.instNeg` `Inner.inner` `InnerProductSpace.toInner` `NormedSpace.normalize`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `AffineMap.map_vadd` `inner_neg_left`
`signedDist_vadd_left_swap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_vadd_left` `signedDist_vadd_right` `inner_neg_right`
`signedDist_vadd_right` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instAdd` `Inner.inner` `InnerProductSpace.toInner` `NormedSpace.normalize`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `ContinuousAffineMap.map_vadd` `signedDist_apply_linear_apply`
`signedDist_vadd_right_swap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_vadd_left_swap` `neg_neg`
`signedDist_vadd_vadd` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_vadd_left_swap` `neg_vadd_vadd`
`signedDist_vsub_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Dist.dist` `PseudoMetricSpace.toDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `signedDist_eq_dist_iff_vsub_mem_span` `Submodule.mem_span_singleton_self`
`signedDist_vsub_self_rev` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real.instNeg` `Dist.dist` `PseudoMetricSpace.toDist`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `neg_eq_iff_eq_neg` `signedDist_neg` `neg_vsub_eq_vsub_rev` `signedDist_vsub_self`
`signedDist_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Real` `Real.instRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul` `Ring.toSemiring` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAffineMap.instAddTorsor` `instIsTopologicalAddTorsor_1` `AffineMap.instFunLike` `signedDist` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real.instZero`	—	`instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddTorsor_1` `smul_zero` `sign_zero` `MulZeroClass.zero_mul` `signedDist_smul`

---

← Back to Index