nfBelow_ofNat

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.nfBelow_ofNat

English

For any natural number n, NFBelow(ofNat n) 1.

Русский

Для любого натурального числа n: NFBelow(ofNat n) 1.

LaTeX

$$$\forall n, \; NFBelow(\mathrm{ofNat}(n), 1)$$$

Lean4

theorem nfBelow_ofNat : ∀ n, NFBelow (ofNat n) 1
  | 0 => NFBelow.zero
  | Nat.succ _ => NFBelow.oadd NF.zero NFBelow.zero zero_lt_one

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

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

Разделы

Аффилиация

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