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
p : P
hp : p ∈ s
p2 : P
⊢ (∃ p2_1, p2_1 ∈ s ∧ p2 -ᵥ p = p2_1 -ᵥ p) ↔ p2 ∈ 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
s : AffineSubspace k P
p : P
hp : p ∈ s
p2 : P
⊢ p2 -ᵥ p ∈ direction s ↔ p2 ∈ s
rw [mem_direction_iff_eq_vsub_right hp]
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
p : P
hp : p ∈ s
p2 : P
⊢ (∃ p2_1, p2_1 ∈ s ∧ p2 -ᵥ p = p2_1 -ᵥ p) ↔ p2 ∈ s
simp