image_const_add_Iio — Mathlib

English

Let α be an ordered additive group. The image of Iio b under x ↦ a + x is Iio(a + b); i.e. { a + x : x < b } = { y ∈ α : y < a + b }.

Русский

Пусть α — упорядоченная аддитивная группа. Образ Iio b при отображении x ↦ a + x равен Iio(a + b); то есть { a + x : x < b } = { y ∈ α : y < a + b }.

LaTeX

$$$$\\{ a + x \\mid x < b \\} = \\{ y \\in \\alpha \\mid y < a + b \\}$$$$

Lean4

theorem image_const_add_Iio : (fun x => a + x) '' Iio b = Iio (a + b) := by simp [add_comm]

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