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
ι : Type ?u.482981
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ ↑s ∧ p₂ ∈ ↑s
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
ι : Type ?u.482981
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ affineSpan k {p₁, p₂} ≤ s
rw [affineSpan_le, Set.insert_subset, Set.singleton_subset_iff]
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
ι : Type ?u.482981
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ ↑s ∧ p₂ ∈ ↑s
exact ⟨hp₁, hp₂⟩