English
There exists a finite subset u of E such that s ⊆ interior(convexHull(u)) ⊆ t for neighborhoods s ⊆ t with s convex and s compact.
Русский
Существует конечное подмножество u ⊆ E такое, что s ⊆ interior(convexHull(u)) ⊆ t при условиях выпуклости s и компактности s.
LaTeX
$$$$\exists u\in Finset(E),\ s\subseteq interior(convexHull_{\mathbb{R}}(u))\land convexHull_{\mathbb{R}}(u)\subseteq t.$$$$
Lean4
/-- We can intercalate a simplex between a point and one of its neighborhoods. -/
theorem exists_mem_interior_convexHull_affineBasis (hs : s ∈ 𝓝 x) :
∃ b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E, x ∈ interior (convexHull ℝ (range b)) ∧ convexHull ℝ (range b) ⊆ s :=
by
classical
-- By translating, WLOG `x` is the origin.
wlog hx : x = 0
· obtain ⟨b, hb⟩ := this (s := -x +ᵥ s) (by simpa using vadd_mem_nhds_vadd (-x) hs) rfl
use x +ᵥ b
simpa [subset_vadd_set_iff, mem_vadd_set_iff_neg_vadd_mem, convexHull_vadd, interior_vadd, Pi.vadd_def,
-vadd_eq_add, vadd_eq_add (a := -x), ← Set.vadd_set_range] using hb
subst hx
obtain ⟨b⟩ :=
exists_affineBasis_of_finiteDimensional (ι := Fin (finrank ℝ E + 1)) (k := ℝ) (P := E)
(by simp)
-- ... translate it to contain the origin...
set c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.univ.centroid ℝ b +ᵥ b
have hc₀ : 0 ∈ interior (convexHull ℝ (range c) : Set E) := by
simpa [c, convexHull_vadd, interior_vadd, range_add, Pi.vadd_def, mem_vadd_set_iff_neg_vadd_mem] using
b.centroid_mem_interior_convexHull
set cnorm := Finset.univ.sup' Finset.univ_nonempty (fun i ↦ ‖c i‖)
have hcnorm : range c ⊆ closedBall 0 (cnorm + 1) := by
simpa only [cnorm, subset_def, Finset.mem_coe, mem_closedBall, dist_zero_right, ← sub_le_iff_le_add,
Finset.le_sup'_iff, forall_mem_range] using fun i ↦
⟨i, by simp⟩
-- ... and finally scale it to fit inside the neighborhood `s`.
obtain ⟨ε, hε, hεs⟩ := Metric.mem_nhds_iff.1 hs
set ε' : ℝ := ε / 2 / (cnorm + 1)
have hc' : 0 < cnorm + 1 :=
by
have : 0 ≤ cnorm := Finset.le_sup'_of_le _ (Finset.mem_univ 0) (norm_nonneg _)
positivity
have hε' : 0 < ε' := by positivity
set d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' hε'.ne' • c
have hε₀ : 0 < ε / 2 := by positivity
have hdnorm : (range d : Set E) ⊆ closedBall 0 (ε / 2) :=
by
simp [d, abs_of_nonneg hε'.le, range_subset_iff, norm_smul]
simpa [ε', hε₀.ne', range_subset_iff, ← mul_div_right_comm (ε / 2), div_le_iff₀ hc', hε₀] using hcnorm
refine ⟨d, ?_, ?_⟩
· simpa [d, Pi.smul_def, range_smul, interior_smul₀, convexHull_smul, zero_mem_smul_set_iff, hε'.ne']
·
calc
convexHull ℝ (range d) ⊆ closedBall 0 (ε / 2) := convexHull_min hdnorm (convex_closedBall ..)
_ ⊆ ball 0 ε := (closedBall_subset_ball (by linarith))
_ ⊆ s := hεs
