exists_affineBasis — Mathlib

English

There exists a subset s of P and an affine basis b on s such that b equals the inclusion of s into P.

Русский

Существует подмножество s пространства P и аффинная база b на s, такая что b совпадает с включением s в P.

LaTeX

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

Lean4

theorem exists_affineBasis : ∃ (s : Set P) (b : AffineBasis (↥s) k P), ⇑b = ((↑) : s → P) :=
  let ⟨s, _, hs⟩ := exists_affine_subbasis (AffineSubspace.span_univ k V P)
  ⟨s, hs⟩

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