preimage_const_sub_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_const_sub_Ioo : (fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b) := by
  simp [← Ioi_inter_Iio, inter_comm]

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