English
From an open set u containing a subset s, there exists a subset t within u that is affinely independent and spans the whole space.
Русский
Из открытого множества u содержащего s существует подмножество t внутри u, которое аффинно независимо и порождает всю пространство.
LaTeX
$$$$\exists s \subseteq u,\ AffineIndependent_{\mathbb{R}}(s) \land \operatorname{affineSpan}_{\mathbb{R}} s = \top.$$$$
Lean4
/-- The affine span of a nonempty open set is `⊤`. -/
theorem affineSpan_eq_top {u : Set P} (hu : IsOpen u) (hne : u.Nonempty) : affineSpan ℝ u = ⊤ :=
let ⟨_, hsu, _, hs'⟩ := hu.exists_subset_affineIndependent_span_eq_top hne
top_unique <| hs' ▸ affineSpan_mono _ hsu