image_sub_const_Iio — 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 < b \} = (-\infty, b - a)$$$

Lean4

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

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