Documentation Verification Report

StrictConvexSpace

📁 Source: Mathlib/Analysis/Convex/StrictConvexSpace.lean

Statistics

Metric	Count
Definitions `StrictConvexSpace`	1
Theorems `instStrictConvexSpace`, `of_norm_add`, `of_norm_add_ne_two`, `of_norm_combo_lt_one`, `of_norm_combo_ne_one`, `of_pairwise_sphere_norm_ne_two`, `of_strictConvex_unitClosedBall`, `strictConvex_closedBall`, `abs_lt_norm_sub_of_not_sameRay`, `combo_mem_ball_of_ne`, `eq_of_norm_eq_of_norm_add_eq`, `lt_norm_sub_of_not_sameRay`, `norm_add_lt_of_not_sameRay`, `norm_combo_lt_of_ne`, `norm_midpoint_lt_iff`, `not_sameRay_iff_abs_lt_norm_sub`, `not_sameRay_iff_norm_add_lt`, `openSegment_subset_ball_of_ne`, `sameRay_iff_norm_add`, `sameRay_iff_norm_sub`, `strictConvexSpace_iff`, `strictConvex_closedBall`	22
Total	23

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instStrictConvexSpace` 📖	mathematical	—	`StrictConvexSpace` `Real` `normedField` `partialOrder` `normedAddCommGroup` `NormedField.toNormedSpace`	—	`strictConvex_iff_convex` `instIsStrictOrderedRing` `instOrderTopologyReal` `convex_closedBall`

StrictConvexSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_norm_add` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`StrictConvexSpace` `Real` `Real.normedField` `Real.partialOrder`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `of_pairwise_sphere_norm_ne_two` `sameRay_iff_of_norm_eq` `mem_sphere_zero_iff_norm`
`of_norm_add_ne_two` 📖	mathematical	—	`StrictConvexSpace` `Real` `Real.normedField` `Real.partialOrder`	—	`Nat.instAtLeastTwoHAddOfNat` `of_norm_combo_ne_one` `LT.lt.le` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `smul_add` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_of_nonneg` `one_div` `div_eq_inv_mul` `div_eq_one_iff_eq` `two_ne_zero'`
`of_norm_combo_lt_one` 📖	mathematical	`Real` `Real.instAdd` `Real.instOne` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField`	`StrictConvexSpace` `Real` `Real.normedField` `Real.partialOrder`	—	`of_strictConvex_unitClosedBall` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.left` `Convex.strictConvex'` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `convex_closedBall` `mem_sphere_zero_iff_norm` `Metric.closedBall_diff_ball` `interior_closedBall` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `AffineMap.lineMap_apply_module` `mem_ball_zero_iff` `sub_eq_iff_eq_add`
`of_norm_combo_ne_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`StrictConvexSpace` `Real` `Real.normedField` `Real.partialOrder`	—	`of_strictConvex_unitClosedBall` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.left` `Convex.strictConvex` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `convex_closedBall` `interior_closedBall` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Metric.closedBall_diff_ball` `frontier_closedBall` `mem_sphere_zero_iff_norm`
`of_pairwise_sphere_norm_ne_two` 📖	mathematical	`Set.Pairwise` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`StrictConvexSpace` `Real` `Real.normedField` `Real.partialOrder`	—	`Nat.instAtLeastTwoHAddOfNat` `of_norm_add_ne_two` `mem_sphere_zero_iff_norm`
`of_strictConvex_unitClosedBall` 📖	mathematical	`StrictConvex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toModule` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne`	`StrictConvexSpace`	—	`smul_unitClosedBall_of_nonneg` `LT.lt.le` `StrictConvex.smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`strictConvex_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StrictConvex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toModule` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—

(root)

Definitions

Name	Category	Theorems
`StrictConvexSpace` 📖	CompData	14 math math: `Submodule.instStrictConvexSpace`, `StrictConvexSpace.of_norm_add_ne_two`, `LinearIsometryEquiv.strictConvexSpace_iff`, `StrictConvexSpace.of_norm_combo_ne_one`, `StrictConvexSpace.of_pairwise_sphere_norm_ne_two`, `StrictConvexSpace.of_strictConvex_unitClosedBall`, `strictConvexSpace_iff`, `UniformConvexSpace.toStrictConvexSpace`, `LinearIsometry.strictConvexSpace`, `LinearIsometry.strictConvexSpace_range_iff`, `LinearIsometry.strictConvexSpace_range`, `Real.instStrictConvexSpace`, `StrictConvexSpace.of_norm_combo_lt_one`, `StrictConvexSpace.of_norm_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_lt_norm_sub_of_not_sameRay` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`Real` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `abs_sub_lt_iff` `Real.instIsOrderedAddMonoid` `lt_norm_sub_of_not_sameRay` `norm_sub_rev` `SameRay.symm`
`combo_mem_ball_of_ne` 📖	mathematical	`Set` `Set.instMembership` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instLT` `Real.instZero` `Real.instAdd` `Real.instOne`	`Set` `Set.instMembership` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField`	—	`eq_or_ne` `Set.mem_singleton_iff` `Metric.closedBall_zero` `interior_closedBall` `strictConvex_closedBall`
`eq_of_norm_eq_of_norm_add_eq` 📖	—	`Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `Real.instAdd`	—	—	`SameRay.eq_of_norm_eq` `Real.instIsStrictOrderedRing` `sameRay_iff_norm_add`
`lt_norm_sub_of_not_sameRay` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`Real` `Real.instLT` `Real.instSub` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `sub_add_cancel` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `norm_add_lt_of_not_sameRay` `SameRay.add_left` `SameRay.rfl`
`norm_add_lt_of_not_sameRay` 📖	mathematical	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAdd`	—	`Real.instIsStrictOrderedRing` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_pos_iff` `combo_mem_ball_of_ne` `inv_norm_smul_mem_unitClosedBall` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `add_div` `div_self` `LT.lt.ne'` `div_lt_one` `div_eq_inv_mul` `Real.norm_of_nonneg` `LT.lt.le` `inv_pos` `norm_smul` `NormedSpace.toNormSMulClass` `smul_add` `smul_inv_smul₀` `SemigroupAction.mul_smul` `mem_ball_zero_iff`
`norm_combo_lt_of_ne` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instLT` `Real.instZero` `Real.instAdd` `Real.instOne`	`Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField`	—	`combo_mem_ball_of_ne`
`norm_midpoint_lt_iff` 📖	mathematical	`Norm.norm` `NormedAddCommGroup.toNorm`	`Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `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` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_of_nonneg` `one_div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zero_le_two` `Real.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_eq_one_div` `div_eq_inv_mul` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `zero_lt_two'` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `mul_two` `not_sameRay_iff_of_norm_eq` `not_sameRay_iff_norm_add_lt`
`not_sameRay_iff_abs_lt_norm_sub` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instLT` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Real.instIsStrictOrderedRing` `Iff.not` `sameRay_iff_norm_sub` `LE.le.lt_iff_ne` `abs_norm_sub_norm_le`
`not_sameRay_iff_norm_add_lt` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Real.instAdd`	—	`Real.instIsStrictOrderedRing` `Iff.not` `sameRay_iff_norm_add` `LE.le.lt_iff_ne` `norm_add_le`
`openSegment_subset_ball_of_ne` 📖	mathematical	`Set` `Set.instMembership` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set` `Set.instHasSubset` `openSegment` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.ball`	—	`openSegment_subset_iff` `combo_mem_ball_of_ne`
`sameRay_iff_norm_add` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Real.instAdd`	—	`Real.instIsStrictOrderedRing` `SameRay.norm_add` `LT.lt.ne` `norm_add_lt_of_not_sameRay`
`sameRay_iff_norm_sub` 📖	mathematical	—	`SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub`	—	`Real.instIsStrictOrderedRing` `SameRay.norm_sub` `LT.lt.ne'` `abs_lt_norm_sub_of_not_sameRay`
`strictConvexSpace_iff` 📖	mathematical	—	`StrictConvexSpace` `StrictConvex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toModule` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`strictConvex_closedBall` 📖	mathematical	—	`StrictConvex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toModule` `Metric.closedBall`	—	`le_or_gt` `Set.Subsingleton.strictConvex` `Metric.subsingleton_closedBall` `vadd_closedBall_zero` `StrictConvex.vadd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `StrictConvexSpace.strictConvex_closedBall`

---

← Back to Index