Iic — Mathlib

English

If f is monotone on a set s, then the map x ↦ Iic (f x) is monotone on s; i.e., for x,y ∈ s with x ≤ y, Iic(f x) ⊆ Iic(f y).

Русский

Пусть f монотонна на множестве s. Тогда отображение x ↦ Iic(f x) монотонно на s: если x ≤ y, то Iic(f x) ⊆ Iic(f y).

LaTeX

$$$\forall x,y \in s,\ 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 : MonotoneOn f s) : MonotoneOn (fun x => Iic (f x)) s :=
  monotone_Iic.comp_monotoneOn hf

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