size_to_nat — Mathlib

English

There is a naturalint size function on Num; its natural-number value equals the Nat.size of the corresponding Num. In particular, for every n, (size n) as a natural equals Nat.size n.

Русский

Существует размерная функция size на Num; её натуральное значение совпадает с Nat.size для соответствующего Num. То есть для каждого n имеем (size n) = Nat.size n.

LaTeX

$$$ (size\, n) = Nat.size\, n $$$

Lean4

theorem size_to_nat : ∀ n, (size n : ℕ) = Nat.size n
  | 0 => Nat.size_zero.symm
  | pos p => p.size_to_nat

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