antitone_Ioi

Mathlib.Order.Interval.Set.Monotone

URI: https://scilib.ai/kg/mathlib#antitone_Ioi

English

The map a ↦ Ioi(a) is antitone: if a ≤ b then Ioi(a) ⊇ Ioi(b).

Русский

Функция a ↦ Ioi(a) антимонотонна: если a ≤ b, тогда Ioi(a) ⊇ Ioi(b).

LaTeX

$$a \\\\le b \\\\Rightarrow Ioi(a) \\\\supseteq Ioi(b)$$

Lean4

theorem antitone_Ioi : Antitone (Ioi : α → Set α) := fun _ _ => Ioi_subset_Ioi

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

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

Разделы

Аффилиация

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