exists_affine_subbasis — Mathlib

English

For any t ⊆ P with a given affine-span-top property, there exists s ⊆ t and an affine basis b on s that aligns with the inclusion of s into P.

Русский

Для любого t ⊆ P с заданным свойством аффинного охвата существует s ⊆ t и аффинная база b на s, согласующаяся с включением s в P.

LaTeX

$$$\\exists s \\subseteq t, \\; \\exists b : AffineBasis s k P, \\; \\forall x \\in s,\\; b(x) = x$$$

Lean4

theorem exists_affine_subbasis {t : Set P} (ht : affineSpan k t = ⊤) :
    ∃ s ⊆ t, ∃ b : AffineBasis s k P, ⇑b = ((↑) : s → P) :=
  by
  obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t
  refine ⟨s, hst, ⟨(↑), h_ind, ?_⟩, rfl⟩
  rw [Subtype.range_coe, h_tot, ht]

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