nat_succ — Mathlib

English

The natural-number successor, when viewed as a cardinal, equals the successor in the cardinal order: (n+1) as Cardinal equals succ(n as Cardinal).

Русский

Переход к следующему числу натурального ряда, рассматриваемый как кардинал, совпадает с порядковым successor: (n+1) в кардинале равен succ(n) в кардинале.

LaTeX

$$$\bigl( (n+1) : \mathrm{Cardinal} \bigr) = \mathrm{succ}(n : \mathrm{Cardinal})$$$

Lean4

@[norm_cast]
theorem nat_succ (n : ℕ) : (n.succ : Cardinal) = succ ↑n :=
  by
  rw [Nat.cast_succ]
  refine (add_one_le_succ _).antisymm (succ_le_of_lt ?_)
  rw [← Nat.cast_succ]
  exact Nat.cast_lt.2 (Nat.lt_succ_self _)

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