canLiftCardinalNat — Mathlib

English

There is a canonical way to lift natural numbers into cardinals: every finite cardinal is the cardinal of some natural number.

Русский

Существуется канонический способ перенести натуральные числа в кардиналы: каждый конечный кардинал равен кардиналу некоторого натурального числа.

LaTeX

$$$ \exists n, (n : Cardinal) = c \text{ for some } c < \aleph_0 $$$

Lean4

instance canLiftCardinalNat : CanLift Cardinal ℕ (↑) fun x => x < ℵ₀ :=
  ⟨fun _ hx =>
    let ⟨n, hn⟩ := lt_aleph0.mp hx
    ⟨n, hn.symm⟩⟩

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