vadd_segment — Mathlib

English

Translation by a fixed vector preserves segments: a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c].

Русский

Сдвиг на фиксированный вектор сохраняет сегменты: a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c].

LaTeX

$$$$ a +\!\!\!\!{\mathbb{V}} [b -[\mathbb{K}] c] = [a +\!\!\!\!{\mathbb{V}} b -[\mathbb{K}] a +\!\!\!\!{\mathbb{V}} c]. $$$$

Lean4

@[simp]
theorem vadd_segment [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) : a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c] :=
  image_segment 𝕜 ⟨_, LinearMap.id, fun _ _ => vadd_comm _ _ _⟩ b c

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