preimage_const_sub_uIcc — Mathlib

English

The preimage of the closed interval [[b, c]] under x ↦ a − x equals the closed interval [[a − b, a − c]] (order taken into account by interval construction).

Русский

Предобраз закрытого интервала [[b, c]] под ↦ a − x равен [[a − b, a − c]] (порядок учитывается конструкцией интервала).

LaTeX

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

Lean4

@[simp]
theorem preimage_const_sub_uIcc : (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]] :=
  by
  simp_rw [← Icc_min_max, preimage_const_sub_Icc]
  simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]
    -- simp can prove this modulo `add_comm`

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