instOrderBot

Mathlib.SetTheory.Ordinal.Basic

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

English

There is a least element in the ordinal order, namely 0, acting as a bottom element.

Русский

Существует наименьший элемент в порядке ординалов, равный 0, выступающий как нижняя граница.

LaTeX

$$$\text{bot} = 0$ and $0 \le o$ for all ordinals o.$$

Lean4

instance : OrderBot Ordinal where
  bot := 0
  bot_le := Ordinal.zero_le

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

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

Разделы

Аффилиация

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