mem_direction_iff_eq_vsub — Mathlib

English

A vector lies in the direction of s iff it can be written as the difference of two points from s.

Русский

Вектор принадлежит направлению s тогда и только тогда, когда его можно записать как разность двух точек из s.

LaTeX

$$$v \\in s.direction \\iff \\exists p_1,p_2 \\in s,\\ v = p_1 -ᵥ p_2$$$

Lean4

/-- A vector is in the direction of a nonempty affine subspace if and only if it is the subtraction
of two vectors in the subspace. -/
theorem mem_direction_iff_eq_vsub {s : AffineSubspace k P} (h : (s : Set P).Nonempty) (v : V) :
    v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂ :=
  by
  rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h, Set.mem_vsub]
  simp only [SetLike.mem_coe, eq_comm]

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