succ_natCast — Mathlib

English

The successor of the natural number n when embedded into cardinals is equal to n plus one in the cardinal arithmetic.

Русский

Переход к следующему числу при вложении в кардиналы равен n+1 в кардинальной арифметике.

LaTeX

$$$\operatorname{succ}(n) = n + 1 \quad \text{in cardinal arithmetic}$$$

Lean4

theorem succ_natCast (n : ℕ) : Order.succ (n : Cardinal) = n + 1 :=
  by
  rw [← Cardinal.nat_succ]
  norm_cast

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