preimage_const_add_uIcc — Mathlib

English

The preimage of the closed interval [[b, c]] under the translation x ↦ a + x equals the closed interval [[b − a, c − a]].

Русский

Предобраз образа x ↦ a + x закрытого интервала [[b, c]] равен [[b − a, c − a]].

LaTeX

$$$ (x \mapsto a + x)^{-1}' [[b, c]] = [[b - a, c - a]] $$$

Lean4

@[simp]
theorem preimage_const_add_uIcc : (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]] := by
  simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]

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