preimage_sub_const_Ico — Mathlib

English

Let α be an ordered additive group. For any a, b, c ∈ α, the preimage of the half-open interval Ico(b, c) under x ↦ x − a is Ico(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 \\le x - a < c \\} = \\{ x \\in \\alpha \\mid b + a \\le x < c + a \\}$$$$

Lean4

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

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