preimage_sub_const_Icc — Mathlib

English

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

Lean4

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

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