affineSpan_eq_top — Mathlib

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

Похожие утверждения