eq_iff_direction_eq_of_mem — Mathlib

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₂⟩⟩

Похожие утверждения