antitone_Ici

Mathlib.Order.Interval.Set.Monotone

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

English

The map a ↦ Ici(a) is antitone with respect to ≤ on α and ⊆ on sets: if a ≤ b then Ici(a) ⊇ Ici(b).

Русский

Функция a ↦ Ici(a) антимонотонна по отношению к ≤ и ⊆: если a ≤ b, то Ici(a) ⊇ Ici(b).

LaTeX

$$a \\\\le b \\\\Rightarrow Iic? No; \\\\Rightarrow Ici(a) \\\\supseteq Ici(b)$$

Lean4

theorem antitone_Ici : Antitone (Ici : α → Set α) := fun _ _ => Ici_subset_Ici.2

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

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

Разделы

Аффилиация

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