preimage_const_sub_Icc — Mathlib

English

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

Русский

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

LaTeX

$$$$\\{ x \\in \\alpha \\mid b \\le a - x \\le c \\} = \\{ x \\in \\alpha \\mid a - c \\le x \\le a - b \\}$$$$

Lean4

@[simp]
theorem preimage_const_sub_Icc : (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b) := by
  simp [← Ici_inter_Iic, inter_comm]

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