Ici

Mathlib.Order.Interval.Set.Monotone

URI: https://scilib.ai/kg/mathlib#Monotone.Ici

English

If f is monotone, then the set-valued map x ↦ Ici(f(x)) is antitone.

Русский

Если f монотонна, то отображение x ↦ Ici(f(x)) антимонотонно.

LaTeX

$$hf : Monotone f \\Rightarrow Antitone (fun x => Ici (f x))$$

Lean4

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

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

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

Разделы

Аффилиация

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