vsub_mem_direction — Mathlib

English

Subtracting two points of an affine subspace yields a vector in its direction.

Русский

Разность двух точек аффинного подпространства дает вектор в его направлении.

LaTeX

$$$\\forall s:\\ AffineSubspace k P, p_1,p_2:\\ P,\\ p_1, p_2 \\in s \\Rightarrow p_1 -ᵥ p_2 \\in s.direction$$$

Lean4

/-- Subtracting two points in the subspace produces a vector in the direction. -/
theorem vsub_mem_direction {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    p₁ -ᵥ p₂ ∈ s.direction :=
  vsub_mem_vectorSpan k hp₁ hp₂

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