preimage_const_sub_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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