coe_toNat_le_self

Mathlib.Data.ENat.Basic

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

English

The natural part of ENat is less than or equal to the ENat value itself: ↑(toNat n) ≤ n.

Русский

Часть toNat(n) в ENat не превосходит само значение n: ↑(toNat n) ≤ n.

LaTeX

$$$\\\\uparrow(\\\\operatorname{toNat}(n)) \\\\le n$$$

Lean4

theorem coe_toNat_le_self (n : ℕ∞) : ↑(toNat n) ≤ n :=
  ENat.recTopCoe le_top (fun _ => le_rfl) n

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

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

Разделы

Аффилиация

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