exists_subset_affineIndependent_span_eq_top

English

Given an open set u and a nonempty open subset s, there exists a finite affine subbasis t within u whose affine span is the whole space.

Русский

Для открытого множества u и непустого подмножества s существует конечная аффинная подбаза t внутри u, такая что affineSpan t = ⊤.

LaTeX

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

Lean4

theorem exists_subset_affineIndependent_span_eq_top {u : Set P} (hu : IsOpen u) (hne : u.Nonempty) :
    ∃ s ⊆ u, AffineIndependent ℝ ((↑) : s → P) ∧ affineSpan ℝ s = ⊤ :=
  by
  rcases hne with ⟨x, hx⟩
  rcases
    hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx) (singleton_nonempty _)
      (affineIndependent_of_subsingleton _ _) with
    ⟨s, -, hsu, hs⟩
  exact ⟨s, hsu, hs⟩

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