zero

Mathlib.Data.Nat.Upto

URI: https://scilib.ai/kg/mathlib#Nat.Upto.zero

← MathLib Explorer

English

Zero is always a member of Nat.Upto(p) since it has no predecessors.

Русский

Ноль всегда принадлежит Nat.Upto(p), потому что у него нет предшественников.

LaTeX

$$$$ 0 \\in \\mathrm{Nat.Upto}(p). $$$$

Lean4

/-- Zero is always a member of `Nat.Upto p` because it has no predecessors. -/
def zero : Nat.Upto p :=
  ⟨0, fun _ h => False.elim (Nat.not_lt_zero _ h)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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