interior_nonempty_iff_affineSpan_eq_top

English

If u is open and nonempty, there exists a subset s ⊆ u with affine independence such that its affine span is the whole space.

Русский

Если u открыто и непусто, существует s ⊆ u, аффинная независимость и аффинная замыкание s = ⊤.

LaTeX

$$$$\exists s \subseteq u,\ AffineIndependent_{\mathbb{R}}((\uparrow) : s \to P) \land \operatorname{affineSpan}_{\mathbb{R}} s = \top.$$$$

Lean4

theorem interior_nonempty_iff_affineSpan_eq_top [FiniteDimensional ℝ V] {s : Set V} (hs : Convex ℝ s) :
    (interior s).Nonempty ↔ affineSpan ℝ s = ⊤ := by
  rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]

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