Theorems · Theorem · functional analysis

convexHull_exists_dist_ge

∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {x : E},
  x ∈ (convexHull ℝ) s → ∀ (y : E), ∃ x' ∈ s, dist x y ≤ dist x' y

Given a point x in the convex hull of s and a point y, there exists a point of s at distance at least dist x y from y.

Defined in

Mathlib.Analysis.Normed.Module.Convex

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedSpace