Theorems · Theorem · convex and discrete geometry

exists_mem_interior_convexHull_affineBasis

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
  s ∈ nhds x → ∃ b, x ∈ interior ((convexHull ℝ) (Set.range ⇑b)) ∧ (convexHull ℝ) (Set.range ⇑b) ⊆ s

We can intercalate a simplex between a point and one of its neighborhoods.

Defined in

Mathlib.Analysis.Normed.Affine.Convex

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional