preimage_sub_const_Ioc — Mathlib

English

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

Lean4

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

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