Iic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem Iic (hf : Monotone f) : Monotone fun x => Iic (f x) :=
  monotone_Iic.comp hf

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