English
Two affine subspaces with the same direction and nonempty intersection are equal.
Русский
Два афинных подпространства с одинаковым направлением и непустым пересечением равны.
LaTeX
$$$s_1.direction = s_2.direction \\rightarrow ((s_1 : Set\\ P) \\cap s_2).Nonempty \\rightarrow s_1 = s_2$$$
Lean4
/-- Two affine subspaces with the same direction and nonempty intersection are equal. -/
theorem ext_of_direction_eq {s₁ s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction)
(hn : ((s₁ : Set P) ∩ s₂).Nonempty) : s₁ = s₂ := by
ext p
have hq1 := Set.mem_of_mem_inter_left hn.some_mem
have hq2 := Set.mem_of_mem_inter_right hn.some_mem
constructor
· intro hp
rw [← vsub_vadd p hn.some]
refine vadd_mem_of_mem_direction ?_ hq2
rw [← hd]
exact vsub_mem_direction hp hq1
· intro hp
rw [← vsub_vadd p hn.some]
refine vadd_mem_of_mem_direction ?_ hq1
rw [hd]
exact vsub_mem_direction hp hq2
