vadd_mem_mk' — Mathlib

English

If v lies in the direction, then v added to p lies in mk' p direction.

Русский

Если v ∈ direction, то v +ᵥ p ∈ mk' p direction.

LaTeX

$$$v \\in \\text{direction} \\Rightarrow (v +\\!\\! v p) \\in \\text{mk}'(p, \\text{direction})$$$

Lean4

/-- An affine subspace constructed from a point and a direction contains the result of adding a
vector in that direction to that point. -/
theorem vadd_mem_mk' {v : V} (p : P) {direction : Submodule k V} (hv : v ∈ direction) : v +ᵥ p ∈ mk' p direction := by
  simpa

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