preimage_sub_const_Ioo — Mathlib

English

Let α be an ordered additive group. For any a, b, c ∈ α, the preimage of the open interval Ioo(b, c) under x ↦ x − a is Ioo(b + a, c + a); i.e. { x ∈ α : b < x − a < c } = { x ∈ α : b + a < x < c + a }.

Русский

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

LaTeX

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

Lean4

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

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