coe_direction_eq_vsub_set_left — Mathlib

English

A vector lies in the direction iff it equals p −ᵥ p2 for some p2 in s.

Русский

Вектор лежит в направлении тогда и только тогда, когда он равен p −ᵥ p2 для некоторой p2 ∈ s.

LaTeX

$$$\\forall s:\\ AffineSubspace k P, p:\\ P, p \\in s \\Rightarrow (v \\in s.direction \\iff \\exists p_2 \\in s, v = p -ᵥ p_2)$$$

Lean4

/-- Given a point in an affine subspace, the set of vectors in its direction equals the set of
vectors subtracting that point on the left. -/
theorem coe_direction_eq_vsub_set_left {s : AffineSubspace k P} {p : P} (hp : p ∈ s) :
    (s.direction : Set V) = (p -ᵥ ·) '' s := by
  ext v
  rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp, Set.mem_image,
    Set.mem_image]
  conv_lhs =>
    congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]

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