toNat_eq_zero

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.toNat_eq_zero

English

toNat n = 0 iff n = 0 or n = ⊤.

Русский

toNat n = 0 эквивалентно n = 0 или n = ⊤.

LaTeX

$$$\\\\operatorname{toNat}(n) = 0 \\\\iff n = 0 \\\\lor n = \\\\top.$$$

Lean4

@[simp]
theorem toNat_eq_zero : toNat n = 0 ↔ n = 0 ∨ n = ⊤ :=
  WithTop.untopD_eq_self_iff

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

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

Разделы

Аффилиация

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