affineSpan_pair_parallel_iff_vectorSpan_eq

English

For four points p1,p2,p3,p4, the line through p1 and p2 is parallel to the line through p3 and p4 if and only if the vector spans of {p1,p2} and {p3,p4} coincide.

Русский

Для четырех точек p1,p2,p3,p4 прямая через p1 и p2 параллельна прямой через p3 и p4 тогда, когда векторные охваты {p1,p2} и {p3,p4} совпадают.

LaTeX

$$$ line[k, p_1, p_2] \\parallel line[k, p_3, p_4] \\iff vectorSpan k ({ p_1, p_2 } : Set P) = vectorSpan k ({ p_3, p_4 } : Set P) $$$

Lean4

theorem affineSpan_pair_parallel_iff_vectorSpan_eq {p₁ p₂ p₃ p₄ : P} :
    line[k, p₁, p₂] ∥ line[k, p₃, p₄] ↔ vectorSpan k ({ p₁, p₂ } : Set P) = vectorSpan k ({ p₃, p₄ } : Set P) := by
  simp [affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, ← not_nonempty_iff_eq_empty]

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