affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial

English

For a nontrivial space, affine span equals top iff vector span equals top.

Русский

Для нетривиального пространства аффинная оболочка равна верхнему пределу тогда и только тогда, когда векторное порождение равно верхнему пределу.

LaTeX

$$$\\text{affineSpan}(k,s)=\\top \\iff \\text{vectorSpan}(k,s)=\\top$$$

Lean4

/-- For a non-trivial space, the affine span of a set is `⊤` iff its vector span is `⊤`. -/
theorem affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial {s : Set P} [Nontrivial P] :
    affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤ :=
  by
  rcases s.eq_empty_or_nonempty with hs | hs
  · simp [hs, subsingleton_iff_bot_eq_top, AddTorsor.subsingleton_iff V P, not_subsingleton]
  · rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]

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