Theorems · Theorem · convex and discrete geometry

StrictConvexSpace.sphere_subset_extremePoints_closedBall

∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : NormedSpace ℝ A] [StrictConvexSpace ℝ A] (a : A) {r : ℝ},
  r ≠ 0 → Metric.sphere a r ⊆ Set.extremePoints ℝ (Metric.closedBall a r)

In a strictly convex space, the sphere is contained in the extreme points of the closed ball when the radius is nonzero. In a nontrivial space, they are equal, see extremePoints_closedBall_eq_sphere.

Defined in

Mathlib.Analysis.Convex.Strict.Extreme

Cited by

0 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceStrictConvexSpace