size_to_nat — Mathlib

English

For any PosNum n, the Nat value of its size equals Nat.size n.

Русский

Для любого PosNum n, натуральное значение размера n равно Nat.size n.

LaTeX

$$$ (size\, n : \mathbb{N}) = \mathrm{Nat.size}(n) $$$

Lean4

theorem size_to_nat : ∀ n, (size n : ℕ) = Nat.size n
  | 1 => Nat.size_one.symm
  | bit0 n =>
    by
    rw [size, succ_to_nat, size_to_nat n, cast_bit0, ← two_mul, ← Nat.bit_false_apply, Nat.size_bit]
    have := to_nat_pos n
    dsimp [Nat.bit]; cutsat
  | bit1 n =>
    by
    rw [size, succ_to_nat, size_to_nat n, cast_bit1, ← two_mul, ← Nat.bit_true_apply, Nat.size_bit]
    dsimp [Nat.bit]; cutsat

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