Parallel — Mathlib

English

Two affine subspaces are parallel if one is obtained from the other by translating all points by the same vector: there exists v ∈ V with s2 = s1.map(constVAdd k P v).

Русский

Два аффиновых подпространства параллельны, если их можно получить друг от друга преобразованием переноса на один и тот же вектор: существует v ∈ V такое, что s2 = s1.map(constVAdd k P v).

LaTeX

$$$ \\exists v \\in V, \\ s_2 = s_1.map (\\text{constVAdd } k P v) $$$

Lean4

/-- Two affine subspaces are parallel if one is related to the other by adding the same vector
to all points. -/
def Parallel (s₁ s₂ : AffineSubspace k P) : Prop :=
  ∃ v : V, s₂ = s₁.map (constVAdd k P v)

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