image_const_sub_Iic — Mathlib

English

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

Русский

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

LaTeX

$$$ \{ a - x \mid x \le b \} = [a - b, \infty)$$$

Lean4

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

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