instOrderBot

Mathlib.Order.Nat

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

English

The natural numbers are equipped with a bottom element 0: 0 is the least natural number.

Русский

Натуральные числа имеют минимальный элемент 0; 0 является наименьшим натуральным числом.

LaTeX

$$$\text{bot}_{\mathbb{N}} = 0$$$

Lean4

instance instOrderBot : OrderBot ℕ where
  bot := 0
  bot_le := zero_le

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

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

Разделы

Аффилиация

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