Ioi — Mathlib

English

If f is monotone, then the map x ↦ Ioi (f(x)) is antitone, i.e., for x ≤ y we have Ioi(f y) ⊆ Ioi(f x).

Русский

Если f монотонна, то отображение x ↦ Ioi(f(x)) антипонтоно: при x ≤ y верно Ioi(f(y)) ⊆ Ioi(f(x)).

LaTeX

$$$\forall x,y \in \alpha,\ x \le y \Rightarrow \{ z \in \beta \mid f(y) < z \} \subseteq \{ z \in \beta \mid f(x) < z \}. $$$

Lean4

protected theorem Ioi (hf : Monotone f) : Antitone fun x => Ioi (f x) :=
  antitone_Ioi.comp_monotone hf

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