English
For sets s1,s2, affineSpan k s1 ∥ affineSpan k s2 if and only if vectorSpan k s1 = vectorSpan k s2 and (s1 = ∅ ↔ s2 = ∅).
Русский
Для множеств s1,s2 выполняется: affineSpan k s1 ∥ affineSpan k s2 тогда и только тогда, когда vectorSpan k s1 = vectorSpan k s2 и (s1 = ∅ ↔ s2 = ∅).
LaTeX
$$$ affineSpan\\ k\\ s_1 \\parallel affineSpan\\ k\\ s_2 \\iff (vectorSpan\\ k\\ s_1 = vectorSpan\\ k\\ s_2) \\land (s_1 = \\emptyset \\iff s_2 = \\emptyset) $$$
Lean4
theorem affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty {s₁ s₂ : Set P} :
affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅) :=
by
repeat rw [← direction_affineSpan, ← affineSpan_eq_bot k]
exact parallel_iff_direction_eq_and_eq_bot_iff_eq_bot
