segment_translate_image — Mathlib

English

The image of the segment [b -[𝕜] c] under translation by a is the segment [a+b -[𝕜] a+c].

Русский

Образ сегмента [b -[𝕜] c] при сдвиге на a есть сегмент [a+b -[𝕜] a+c].

LaTeX

$$$$ (\lambda x. a+x) '' [b -[\mathbb{K}] c] = [a + b -[\mathbb{K}] a + c]. $$$$

Lean4

theorem segment_translate_image (a b c : E) : (fun x => a + x) '' [b -[𝕜] c] = [a + b -[𝕜] a + c] :=
  segment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ <| add_left_surjective a

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