English
Parallelism of affine spans implies equality of their vector spans, and emptiness of the original sets are aligned: affineSpan k s1 ∥ affineSpan k s2 iff vectorSpan k s1 = vectorSpan k 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) \\wedge (s_1 = \\emptyset \\iff s_2 = \\emptyset) $$$
Lean4
theorem parallel_iff_direction_eq_and_eq_bot_iff_eq_bot {s₁ s₂ : AffineSubspace k P} :
s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥) :=
by
refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
· rintro rfl
exact bot_parallel_iff_eq_bot.1 h
· rintro rfl
exact parallel_bot_iff_eq_bot.1 h
· rcases h with ⟨hd, hb⟩
by_cases hs₁ : s₁ = ⊥
· rw [hs₁, bot_parallel_iff_eq_bot]
exact hb.1 hs₁
· have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
rcases (nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩
rcases (nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩
refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩
· rw [mem_map]
refine ⟨p₁, hp₁, ?_⟩
simp
· simpa using hd.symm
