preimage_const_sub_Ioc — Mathlib

English

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

Русский

Пусть α — упорядоченная аддитивная группа. При отображении x ↦ a − x прообраз Ioc(b, c) равен Ico(a − c, a − b); т.е. { x ∈ α : b < a − x ≤ c } = [a − c, a − b).

LaTeX

$$$$\\{ x \\in \\alpha \\mid b < a - x \\le c \\} = \\mathrm{Ico}(a - c, a - b)$$$$

Lean4

@[simp]
theorem preimage_const_sub_Ioc : (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b) := by
  simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]

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