k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (affineSpan k (↑s ∪ ↑(affineSpan k {p2}))) = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (affineSpan k (insert p2 ↑s)) = Submodule.span k {p2 -ᵥ p1} ⊔ direction s
rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p2]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (s ⊔ affineSpan k {p2}) = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (affineSpan k (↑s ∪ ↑(affineSpan k {p2}))) = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
change (s ⊔ affineSpan k {p2}).direction = _
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction s ⊔ vectorSpan k {p2} ⊔ Submodule.span k {p2 -ᵥ p1} = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction (s ⊔ affineSpan k {p2}) = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
rw [direction_sup hp1 (mem_affineSpan k (Set.mem_singleton _)), direction_affineSpan]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p1 p2 : P
hp1 : p1 ∈ s
⊢ direction s ⊔ vectorSpan k {p2} ⊔ Submodule.span k {p2 -ᵥ p1} = direction s ⊔ Submodule.span k {p2 -ᵥ p1}
simp