instOrderBot

Mathlib.Data.Finset.Empty

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

English

The empty Finset is the bottom element with respect to inclusion: ∅ ⊆ s for every Finset s.

Русский

Пустой Finset является нижним элементом относительно включения: ∅ ⊆ s для любого Finset s.

LaTeX

$$$ \emptyset \subseteq s \quad \text{for all } s, \,$$

Lean4

instance : OrderBot (Finset α) where
  bot := ∅
  bot_le := empty_subset

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

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

Разделы

Аффилиация

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