not_isSuccLimit_natCast — Mathlib

English

For every natural number n, n viewed as a cardinal is not IsSuccLimit.

Русский

Для каждого натурального числа n, рассматриваемого как кардинал, не выполняется IsSuccLimit.

LaTeX

$$$\forall n \in \mathbb{N},\ \lnot IsSuccLimit(n) $$$

Lean4

theorem not_isSuccLimit_natCast : (n : ℕ) → ¬IsSuccLimit (n : Cardinal.{u})
  | 0, e => e.1 isMin_bot
  | Nat.succ n, e => Order.not_isSuccPrelimit_succ _ (nat_succ n ▸ e.2)

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