vadd_mem_iff_mem_direction — Mathlib

English

A vector added to a point in s lies in s iff the vector lies in the direction of s.

Русский

Вектор, добавляемый к точке из s, принадлежит s тогда и только тогда, когда вектор принадлежит направлению s.

LaTeX

$$$\\forall s:\\ AffineSubspace k P, v:\\ V, p:\\ P, p \\in s \\Rightarrow (v +_{\\mathrm{v}} p \\in s \\iff v \\in s.direction)$$$

Lean4

/-- Adding a vector to a point in a subspace produces a point in the subspace if and only if the
vector is in the direction. -/
theorem vadd_mem_iff_mem_direction {s : AffineSubspace k P} (v : V) {p : P} (hp : p ∈ s) :
    v +ᵥ p ∈ s ↔ v ∈ s.direction :=
  ⟨fun h => by simpa using vsub_mem_direction h hp, fun h => vadd_mem_of_mem_direction h hp⟩

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