image_const_sub_Ico — Mathlib

English

Let α be an ordered additive group. For any b ≤ c, the image of the half-open interval [b, c) under x ↦ a − x is (a − c, a − b].

Русский

Пусть α — упорядоченная аддитивная группа. Для любых b ≤ c образ [b, c) при отображении x ↦ a − x равен (a − c, a − b].

LaTeX

$$$ \{ a - x \mid x \in [b, c) \} = (a - c, a - b]$$

Lean4

@[simp]
theorem image_const_sub_Ico : (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b) :=
  by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]

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