openSegment_translate_preimage — Mathlib

English

The preimage of an open segment under translation is the open segment.

Русский

Предобраз открытого сегмента под действием сдвига равен открытому сегменту.

LaTeX

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

Lean4

theorem openSegment_translate_preimage (a b c : E) :
    (fun x => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c :=
  Set.ext fun _ => mem_openSegment_translate 𝕜 a

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