preimage_const_sub_Ici — Mathlib

English

Let α be an ordered additive group. For any a, b ∈ α, the preimage of Ici b under the map x ↦ a − x is Iic(a − b); namely { x ∈ α : a − x ≥ b } = { x ∈ α : x ≤ a − b }.

Русский

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

LaTeX

$$$$\\{ x \\in \\alpha \\mid a - x \\in \\mathrm{Ici}(b) \\} = \\mathrm{Iic}(a - b)$$$$

Lean4

@[simp]
theorem preimage_const_sub_Ici : (fun x => a - x) ⁻¹' Ici b = Iic (a - b) :=
  ext fun _x => le_sub_comm

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