English
An affine subspace from a point and a direction consists of all points whose displacement from the point lies in the direction.
Русский
Афинное подпространство, заданное точкой и направлением, состоит из всех точек, разность которых с данной точкой лежит в направлении.
LaTeX
$$$\\text{mk}'(p, \\text{direction}) = \\{ q \\in P \\mid q -\\!\\! v p \\in \\text{direction} \\}$$$
Lean4
/-- Two affine subspaces with nonempty intersection are equal if and only if their directions are
equal. -/
theorem eq_iff_direction_eq_of_mem {s₁ s₂ : AffineSubspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) :
s₁ = s₂ ↔ s₁.direction = s₂.direction :=
⟨fun h => h ▸ rfl, fun h => ext_of_direction_eq h ⟨p, h₁, h₂⟩⟩