floor_toNat

Mathlib.Algebra.Order.Floor.Defs

URI: https://scilib.ai/kg/mathlib#Int.floor_toNat

English

The same identity with Nat.floor: toNat(⌊a⌋) = Nat.floor(a).

Русский

Та же аналогия: toNat(⌊a⌋) = Nat.floor(a).

LaTeX

$$$\operatorname{toNat}(\lfloor a \rfloor) = \operatorname{Nat}.floor(a).$$$

Lean4

theorem floor_toNat (a : α) : ⌊a⌋.toNat = ⌊a⌋₊ :=
  rfl

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

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

Разделы

Аффилиация

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