vectorSpan_eq_top_of_affineSpan_eq_top

English

For a nonempty set s, affineSpan k s = ⊤ iff vectorSpan k s = ⊤.

Русский

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

LaTeX

$$s.Nonempty → (affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤)$$

Lean4

/-- If the affine span of a set is `⊤`, then the vector span of the same set is the `⊤`. -/
theorem vectorSpan_eq_top_of_affineSpan_eq_top {s : Set P} (h : affineSpan k s = ⊤) : vectorSpan k s = ⊤ := by
  rw [← direction_affineSpan, h, direction_top]

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