English
If f is monotone, then x ↦ Iio (f(x)) is monotone, i.e., for x ≤ y we have Iio(f x) ⊆ Iio(f y).
Русский
Если f монотонна, то x ↦ Iio(f(x)) монотонна: при x ≤ y выполняется Iio(f x) ⊆ Iio(f y).
LaTeX
$$$\forall x,y \in \alpha,\ x \le y \Rightarrow \{ z \in \beta \mid f(x) < z \} \subseteq \{ z \in \beta \mid f(y) < z \}. $$$
Lean4
protected theorem Iio (hf : Monotone f) : Monotone fun x => Iio (f x) :=
monotone_Iio.comp hf