instOrderBot

Mathlib.Combinatorics.Colex

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

English

There is a bottom element in the Colex order given by the image of the empty Finset: bot = toColex ∅.

Русский

В порядке Colex существует нижний элемент, равный образу пустого множества: bot = toColex ∅.

LaTeX

$$$\bot = toColex(\emptyset)$$$

Lean4

instance instOrderBot : OrderBot (Colex (Finset α))
    where
  bot := toColex ∅
  bot_le s a ha := by cases ha

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

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

Разделы

Аффилиация

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