image_sub_const_Ici — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_sub_const_Ici : (fun x => x - a) '' Ici b = Ici (b - a) := by simp [sub_eq_neg_add]

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