Ioi

Mathlib.Order.Interval.Set.Monotone

URI: https://scilib.ai/kg/mathlib#AntitoneOn.Ioi

English

If f is antitone on s, then x ↦ Ioi (f x) is monotone on s.

Русский

Если f антимонотонна на s, то x ↦ Ioi(f x) монотонно на s.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru