preimage_const_sub_Iic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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