mem_mk' — Mathlib

English

A point lies in mk' p direction exactly when its velocity from p lies in direction.

Русский

Точка q принадлежит mk' p direction тогда и только тогда, когда q -ᵥ p ∈ direction.

LaTeX

$$$q \\in \\text{mk}'(p, \\text{direction}) \\iff q -\\!\\! v p \\in \\text{direction}$$$

Lean4

/-- A point lies in an affine subspace constructed from another point and a direction if and only
if their difference is in that direction. -/
@[simp]
theorem mem_mk' {p q : P} {direction : Submodule k V} : q ∈ mk' p direction ↔ q -ᵥ p ∈ direction :=
  Iff.rfl

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