subset_Iic_sup_id

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.subset_Iic_sup_id

English

For any finite s, every element of s is ≤ the supremum of s under the identity, i.e., s ⊆ Iic (s.sup id).

Русский

Для любого конечного множества s каждый элемент не превышает максимум s; то есть s ⊆ Iic (s.sup id).

LaTeX

$$$ s \subseteq Iic (s.sup id) $$$

Lean4

theorem subset_Iic_sup_id [OrderBot α] (s : Finset α) : s ⊆ Iic (s.sup id) := fun _ h ↦ mem_Iic.2 <| le_sup (f := id) h

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

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

Разделы

Аффилиация

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