preimage_sub_const_Iio — Mathlib

English

Let α be an ordered additive group. For any a, b ∈ α, the preimage of the lower interval { x ∈ α : x < b } under the translation x ↦ x − a is the interval { x ∈ α : x < b + a }, i.e. { x ∈ α | x − a < b } = { x ∈ α | x < b + a }.

Русский

Пусть α — упорядоченная аддитивная группа. Для любых a, b ∈ α верно: { x ∈ α | x − a < b } = { x ∈ α | x < b + a }. Множество сохраняет порядок при сдвиге на a.

LaTeX

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

Lean4

@[simp]
theorem preimage_sub_const_Iio : (fun x => x - a) ⁻¹' Iio b = Iio (b + a) := by simp [sub_eq_add_neg]

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