image_const_sub_Ici — Mathlib

English

Let α be an ordered additive group. For any a, b ∈ α, the image of the interval [b, ∞) under the map x ↦ a − x is (−∞, a − b].

Русский

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

LaTeX

$$$ \{ a - x \mid x \ge b \} = (-\infty, a - b]$$$

Lean4

@[simp]
theorem image_const_sub_Ici : (fun x => a - x) '' Ici b = Iic (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]

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