openSegment_translate_image — Mathlib

English

The image of an open segment under x ↦ a+x is the open segment between a+b and a+c.

Русский

Образ открытого сегмента при сдвиге на a равен открытому сегменту между a+b и a+c.

LaTeX

$$$$ (\lambda x. a+x) '' openSegment_{\mathbb{K}}(b,c) = openSegment_{\mathbb{K}}(a+b,a+c). $$$$

Lean4

theorem openSegment_translate_image (a b c : E) :
    (fun x => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c) :=
  openSegment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ <| add_left_surjective a

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