vadd_mem_iff_mem_of_mem_direction

English

The same as above: adding a direction vector to a point in a subspace stays in the subspace.

Русский

То же самое: прибавление вектора направления к точке остаётся внутри подпространства.

LaTeX

$$$v +_{\\mathrm{v}} p \\in s \\iff p \\in s$$$

Lean4

/-- Adding a vector in the direction to a point produces a point in the subspace if and only if
the original point is in the subspace. -/
theorem vadd_mem_iff_mem_of_mem_direction {s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction) {p : P} :
    v +ᵥ p ∈ s ↔ p ∈ s := by
  refine ⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩
  convert vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h
  simp

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