Iio — Mathlib

English

If f is antitone, then x ↦ Iio (f x) is antitone, i.e., for x ≤ y we have Iio(f y) ⊆ Iio(f x).

Русский

Если f антимонотонна, то x ↦ Iio(f x) антитонична: при x ≤ y выполняется Iio(f y) ⊆ Iio(f x).

LaTeX

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

Lean4

protected theorem Iio (hf : Antitone f) : Antitone fun x => Iio (f x) :=
  monotone_Iio.comp_antitone hf

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