vectorSpan_eq — Mathlib

English

If two affine subspaces S1 and S2 are parallel, then their vector spans are equal: vectorSpan k S1 = vectorSpan k S2.

Русский

Если два аффиновых подпространства параллельны, то их векторные охваты равны: vectorSpan k S1 = vectorSpan k S2.

LaTeX

$$$ (S_1 \\parallel S_2) \\Rightarrow (vectorSpan\\ k\\ S_1 = vectorSpan\\ k\\ S_2) $$$

Lean4

theorem vectorSpan_eq {s₁ s₂ : Set P} (h : affineSpan k s₁ ∥ affineSpan k s₂) : vectorSpan k s₁ = vectorSpan k s₂ :=
  by
  simp_rw [← direction_affineSpan]
  exact h.direction_eq

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