zero_le

Mathlib.SetTheory.Ordinal.Basic

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

English

Every ordinal is nonnegative; in particular, 0 is the least ordinal.

Русский

Каждый ординал неотрицателен; в частности, 0 — наименьший ординал.

LaTeX

$$$0 \le o\quad\text{for all } o\in\operatorname{Ordinal}.$$$

Lean4

protected theorem zero_le (o : Ordinal) : 0 ≤ o :=
  inductionOn o fun _ r _ => (InitialSeg.ofIsEmpty _ r).ordinal_type_le

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

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

Разделы

Аффилиация

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