lt_aleph0 — Mathlib

English

c < aleph0 iff there exists n with c = n.

Русский

c < aleph0 тогда и только если существует n такое, что c = n.

LaTeX

$$$c < \aleph_0 \iff \exists n \in \mathbb{N}, c = n$$$

Lean4

theorem lt_aleph0 {c : Cardinal} : c < ℵ₀ ↔ ∃ n : ℕ, c = n :=
  ⟨fun h => by
    rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩
    rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩
    suffices S.Finite by
      lift S to Finset ℕ using this
      simp
    contrapose! h'
    haveI := Infinite.to_subtype h'
    exact ⟨Infinite.natEmbedding S⟩, fun ⟨_, e⟩ => e.symm ▸ nat_lt_aleph0 _⟩

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