k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    direction (affineSpan k s₁) = direction (affineSpan k s₂) ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
repeat rw [← direction_affineSpan, ← affineSpan_eq_bot k]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    direction (affineSpan k s₁) = direction (affineSpan k s₂) ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
exact parallel_iff_direction_eq_and_eq_bot_iff_eq_bot
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    direction (affineSpan k s₁) = direction (affineSpan k s₂) ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    direction (affineSpan k s₁) = direction (affineSpan k s₂) ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
rw [← direction_affineSpan, ← affineSpan_eq_bot k]