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