Theorems · Theorem · convex and discrete geometry

Convex.exists_subset_interior_convexHull_finset_of_isCompact

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s t : Set E},
  Convex ℝ s → IsCompact s → t ∈ nhdsSet s → ∃ u, s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t

We can intercalate a convex polytope between a compact convex set and one of its neighborhoods.

Defined in

Mathlib.Analysis.Normed.Affine.Convex

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional