Ici — Mathlib

English

Let f be antitone on a set s ⊆ α. Then the set-valued map x ↦ Ici (f x) is monotone on s, i.e., for x,y ∈ s with x ≤ y, Ici(f x) ⊆ Ici(f y).

Русский

Пусть f антимонотонна на множестве s ⊆ α. Тогда отображение x ↦ Ici(f(x)) монотонно на s, т.е. для x,y ∈ s с x ≤ y выполняется Ici(f(x)) ⊆ Ici(f(y)).

LaTeX

$$$\forall x,y \in s,\ x \le y \Rightarrow \Ici(f(x)) \subseteq \Ici(f(y)).$$$

Lean4

protected theorem Ici (hf : AntitoneOn f s) : MonotoneOn (fun x => Ici (f x)) s :=
  antitone_Ici.comp_antitoneOn hf

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