Documentation Verification Report

Convex

📁 Source: Mathlib/Analysis/Normed/Module/Convex.lean

Statistics

Metric	Count
Definitions `Convex`	1
Theorems `cthickening`, `thickening`, `segment_of_prod_nhds`, `segment_of_prod_nhdsWithin`, `instPathConnectedSpace`, `convexHull_diam`, `convexHull_ediam`, `convexHull_exists_dist_ge`, `convexHull_exists_dist_ge2`, `convexHull_sphere_eq_closedBall`, `convexOn_dist`, `convexOn_norm`, `convexOn_univ_dist`, `convexOn_univ_norm`, `convex_ball`, `convex_closedBall`, `convex_closedEBall`, `convex_eball`, `isBounded_convexHull`, `isConnected_setOf_sameRay`, `isConnected_setOf_sameRay_and_ne_zero`, `norm_sub_le_of_mem_segment`, `segment_subset_closedBall_left`, `segment_subset_closedBall_right`	24
Total	25

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cthickening` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`le_total` `Metric.cthickening_eq_iInter_thickening` `convex_iInter₂` `thickening` `Metric.cthickening_of_nonpos` `closure` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`thickening` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`add_ball_zero` `add` `convex_ball`

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`segment_of_prod_nhds` 📖	—	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd`	—	—	`Metric.eventually_prod_nhds_iff` `Filter.mp_mem` `Metric.tendsto_nhds` `Filter.univ_mem'` `convex_iff_segment_subset` `convex_ball`
`segment_of_prod_nhdsWithin` 📖	—	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd` `nhdsWithin` `Set` `Set.instHasSubset` `segment` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	—	—	`mp` `mono` `segment_of_prod_nhds` `Filter.comap_inf` `Filter.comap_principal` `forall₂_imp`

NormedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPathConnectedSpace` 📖	mathematical	—	`PathConnectedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`IsTopologicalAddGroup.pathConnectedSpace` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `toIsBoundedSMul`

(root)

Definitions

Name	Category	Theorems
`Convex` 📖	MathDef	137 math math: `ConvexCone.convex`, `strictConvexOn_iff_slope_strict_mono_adjacent`, `quasiconcaveOn_iff_min_le`, `convex_iff_ordConnected`, `QuasiconvexOn.convex_lt`, `concaveOn_iff_slope_anti_adjacent`, `ProperCone.convex`, `convex_iff_sum_mem`, `convexHull_eq_iInter`, `convex_iff_pairwise_pos`, `convex_Iic`, `Metric.exists_forall_closedEBall_subset_aux₂`, `coe_convexAddSubmonoid`, `locallyConvexSpace_iff`, `Antitone.convex_le`, `ConcaveOn.convex_ge`, `LocallyConvexSpace.convex_basis_zero`, `QuasiconcaveOn.convex_gt`, `convex_iff_openSegment_subset`, `Monotone.convex_ge`, `convex_iff_add_mem`, `convex_singleton`, `ConcaveOn.convex_strict_hypograph`, `convex_halfSpace_re_le`, `convexOn_iff_forall_pos`, `convex_Ico`, `Antitone.convex_lt`, `convex_halfSpace_im_gt`, `ConvexBody.convex`, `EMetric.exists_forall_closedBall_subset_aux₂`, `ConvexOn.convex_epigraph`, `convex_halfSpace_ge`, `quasiconvexOn_iff_le_max`, `convex_openSegment`, `Antitone.convex_ge`, `convex_eball`, `StrictConcaveOn.convex_gt`, `EuclideanHalfSpace.convex`, `concaveOn_iff_div`, `IsPreconnected.convex`, `Set.OrdConnected.convex`, `convex_halfSpace_im_lt`, `Matrix.convex_colStochastic`, `strictConvex_iff_convex`, `Monotone.convex_lt`, `AffineSubspace.convex`, `PointedCone.convex`, `Set.Subsingleton.convex`, `convex_Ioo`, `EuclideanQuadrant.convex`, `Set.OrdConnected.convex_of_chain`, `ConvexOn.convex_lt`, `convex_convexHull`, `strictConcaveOn_iff_slope_strict_anti_adjacent`, `ConcaveOn.convex_hypograph`, `Seminorm.convex_ball`, `convex_closedEBall`, `ConvexOn.convex_re_epigraph`, `convex_ball`, `convex_absConvexHull`, `Real.convex_iff_isPreconnected`, `Submodule.convex`, `convex_halfSpace_re_ge`, `convex_uIcc`, `convex_halfSpace_im_ge`, `convex_Icc`, `convex_halfSpace_re_lt`, `ModelWithCorners.convex_range`, `ConvexOn.convex_le`, `Antitone.convex_gt`, `convex_univ`, `convex_hyperplane`, `NNReal.convex_iff`, `StrictConvexOn.convex_lt`, `convex_RCLike_iff_convex_real`, `convex_empty`, `convex_stdSimplex`, `convex_parallelepiped`, `IsOpen.strictConvex_iff`, `QuasiconvexOn.convex`, `NumberField.mixedEmbedding.convexBodyLT_convex`, `convex_Ici`, `convex_setOf_holderWith`, `concaveOn_iff_pairwise_pos`, `ModelWithCorners.convex_range'`, `convex_Iio`, `convex_halfSpace_gt`, `Convex_subadditive_le`, `convex_iff_div`, `convex_iff_pointwise_add_subset`, `convex_Ioc`, `Matrix.convex_rowStochastic`, `LocallyConvexSpace.convex_open_basis_zero`, `convex_iff_segment_subset`, `concaveOn_iff_forall_pos`, `strictConcaveOn_iff_div`, `ConvexBody.convex'`, `convex_halfSpace_le`, `ConvexOn.convex_strict_epigraph`, `convexHull_isClosed`, `quasilinearOn_iff_mem_uIcc`, `convex_doublyStochastic`, `StrictConvex.convex`, `LocallyConvexSpace.convex_basis`, `convex_setOf_holderOnWith`, `AbsConvexOpenSets.coe_convex`, `NumberField.mixedEmbedding.convexBodySum_convex`, `convex_halfSpace_im_le`, `Monotone.convex_le`, `locallyConvexSpace_iff_zero`, `Submodule.Convex.semilinear_range`, `convex_vadd`, `convexOn_iff_div`, `strictConvexOn_iff_div`, `concaveOn_iff_convex_hypograph`, `convex_halfSpace_lt`, `convex_halfSpace_re_gt`, `QuasiconcaveOn.convex`, `Seminorm.convex_closedBall`, `convex_zero`, `convex_closedConvexHull`, `convex_Ioi`, `convex_iff_forall_pos`, `convexHull_eq_self`, `convex_closedBall`, `convexOn_iff_convex_epigraph`, `ConcaveOn.convex_gt`, `ProbabilityTheory.convex_integrableExpSet`, `mem_convexAddSubmonoid`, `NumberField.mixedEmbedding.convexBodyLT'_convex`, `locallyConvexSpace_iff_exists_convex_subset_zero`, `convexOn_iff_pairwise_pos`, `convex_segment`, `closedConvexHull_isClosed`, `Monotone.convex_gt`, `convexOn_iff_slope_mono_adjacent`, `locallyConvexSpace_iff_exists_convex_subset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexHull_diam` 📖	mathematical	—	`Metric.diam` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ClosureOperator` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	—	`convexHull_ediam`
`convexHull_ediam` 📖	mathematical	—	`Metric.ediam` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ClosureOperator` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	—	`LE.le.antisymm` `Metric.ediam_le` `convexHull_exists_dist_ge2` `edist_dist` `le_trans` `ENNReal.ofReal_le_ofReal` `Metric.edist_le_ediam_of_mem` `Metric.ediam_mono` `subset_convexHull`
`convexHull_exists_dist_ge` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ConvexOn.exists_ge_of_mem_convexHull` `Real.instIsStrictOrderedRing` `Real.instIsOrderedAddMonoid` `IsStrictOrderedRing.toIsStrictOrderedModule` `convexOn_dist` `convex_convexHull` `subset_convexHull`
`convexHull_exists_dist_ge2` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`convexHull_exists_dist_ge` `le_trans` `dist_comm`
`convexHull_sphere_eq_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`DFunLike.coe` `ClosureOperator` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Metric.sphere` `Metric.closedBall`	—	`subset_antisymm` `Set.instAntisymmSubset` `convexHull_min` `Metric.sphere_subset_closedBall` `convex_closedBall` `mem_convexHull_iff` `Nat.instAtLeastTwoHAddOfNat` `NormedSpace.sphere_nonempty` `EMetric.instNontrivialTopologyOfNontrivial` `midpoint_self_neg` `Convex.midpoint_mem` `Real.instIsStrictOrderedRing` `sub_zero` `norm_neg` `Metric.closedBall_zero` `le_imp_le_of_le_of_le` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_zero_right` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `lt_of_le_of_ne'` `le_refl` `inv_mul_le_one` `Real.instZeroLEOneClass` `norm_smul` `NormedSpace.toNormSMulClass` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `norm_norm` `inv_mul_cancel_right₀` `Real.instIsOrderedAddMonoid` `StarConvex.smul_mem` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Convex.starConvex` `mul_pos` `norm_pos_iff` `one_smul` `inv_mul_cancel₀` `mul_one` `mul_assoc` `mul_comm` `smul_eq_mul` `smul_assoc` `IsScalarTower.left` `add_zero` `vadd_eq_add` `Metric.vadd_sphere` `NormedAddGroup.to_isIsometricVAdd_left` `convexHull_vadd` `vadd_closedBall_zero`
`convexOn_dist` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`ConvexOn` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`dist_eq_norm` `Set.image_add_left` `neg_neg` `Set.preimage_preimage` `add_sub_cancel` `ConvexOn.comp_affineMap` `convexOn_norm` `Convex.translate`
`convexOn_norm` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`ConvexOn` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`norm_add_le` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_of_nonneg`
`convexOn_univ_dist` 📖	mathematical	—	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`convexOn_dist` `convex_univ`
`convexOn_univ_norm` 📖	mathematical	—	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`convexOn_norm` `convex_univ`
`convex_ball` 📖	mathematical	—	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Set.sep_univ` `ConvexOn.convex_lt` `Real.instIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `convexOn_univ_dist`
`convex_closedBall` 📖	mathematical	—	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Set.sep_univ` `ConvexOn.convex_le` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `convexOn_univ_dist`
`convex_closedEBall` 📖	mathematical	—	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.closedEBall` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Metric.closedEBall_top` `Metric.closedEBall_coe`
`convex_eball` 📖	mathematical	—	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.eball` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Metric.eball_top` `Metric.eball_coe`
`isBounded_convexHull` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ClosureOperator` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	—	`convexHull_ediam`
`isConnected_setOf_sameRay` 📖	mathematical	—	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `setOf` `SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	—	`Real.instIsStrictOrderedRing` `SameRay.congr_simp` `isConnected_univ` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `exists_nonneg_left_iff_sameRay` `IsConnected.image` `isConnected_Ici` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuousOn_id'` `continuousOn_const`
`isConnected_setOf_sameRay_and_ne_zero` 📖	mathematical	—	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `setOf` `SameRay` `Real` `Real.instCommSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Real.instIsStrictOrderedRing` `exists_pos_left_iff_sameRay_and_ne_zero` `IsConnected.image` `isConnected_Ioi` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuousOn_id'` `continuousOn_const`
`norm_sub_le_of_mem_segment` 📖	mathematical	`Set` `Set.instMembership` `segment` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub`	—	`segment_eq_image'` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_sub_cancel_left` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_nonneg` `one_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg`
`segment_subset_closedBall_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `segment` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Convex.segment_subset` `convex_closedBall` `Metric.mem_closedBall_self` `dist_nonneg` `Metric.mem_closedBall` `le_refl` `dist_comm`
`segment_subset_closedBall_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `segment` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`segment_symm` `segment_subset_closedBall_left` `dist_comm`

---

← Back to Index