vadd_mem_of_mem_direction — Mathlib

English

Adding a direction vector to a point in a subspace yields another point in the subspace.

Русский

Прибавление вектора направления к точке подпространства даёт другую точку в подпространстве.

LaTeX

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

Lean4

/-- Adding a vector in the direction to a point in the subspace produces a point in the
subspace. -/
theorem vadd_mem_of_mem_direction {s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction) {p : P} (hp : p ∈ s) :
    v +ᵥ p ∈ s := by
  rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv
  rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩
  rw [hv]
  convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp
  rw [one_smul]

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