k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Coplanar k (insert p s)
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
⊢ Coplanar k (insert p s)
have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_vectorSpan
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p s) } ≤ 2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Coplanar k (insert p s)
rw [coplanar_iff_finrank_le_two]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ finrank k { x // x ∈ vectorSpan k (insert p s) } ≤ 2
exact (finrank_vectorSpan_insert_le_set k s p).trans (add_le_add_right h.finrank_le_one _)