segment_translate_preimage — Mathlib

English

The preimage of the translated segment under x ↦ a+x equals the original segment.

Русский

Образ под обратным переводом сегмента равен исходному сегменту.

LaTeX

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

Lean4

theorem segment_translate_preimage (a b c : E) : (fun x => a + x) ⁻¹' [a + b -[𝕜] a + c] = [b -[𝕜] c] :=
  Set.ext fun _ => mem_segment_translate 𝕜 a

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