Ici — Mathlib

English

Let f: α → β be antitone. Then the set-valued map x ↦ {y ∈ β | f(x) ≤ y} is monotone in x (with respect to ≤ on α and ⊆ on sets). Equivalently, for all x ≤ y, {z ∈ β | f(x) ≤ z} ⊆ {z ∈ β | f(y) ≤ z}.

Русский

Пусть f: α → β антимонотонна. Тогда отображение x ↦ {y ∈ β | f(x) ≤ y} монотонно по x (относительно ⊆ на множествах). Эквивалентно: если x ≤ y, то {z ∈ β | f(x) ≤ z} ⊆ {z ∈ β | f(y) ≤ z}.

LaTeX

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

Lean4

protected theorem Ici (hf : Antitone f) : Monotone fun x => Ici (f x) :=
  antitone_Ici.comp hf

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