preimage_const_sub_Ioi — Mathlib

English

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

Русский

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

LaTeX

$$$$\\{ x \\in \\alpha \\mid a - x \\in \\mathrm{Ioi}(b) \\} = \\mathrm{Iio}(a - b)$$$$

Lean4

@[simp]
theorem preimage_const_sub_Ioi : (fun x => a - x) ⁻¹' Ioi b = Iio (a - b) :=
  ext fun _x => lt_sub_comm

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