aleph0_le — Mathlib

English

aleph0 ≤ c iff every natural n satisfies n ≤ c.

Русский

aleph0 ≤ c тогда и только если для каждого n ∈ ℕ выполняется n ≤ c.

LaTeX

$$$\aleph_0 \le c \iff \forall n \in \mathbb{N},\ n \le c$$$

Lean4

theorem aleph0_le {c : Cardinal} : ℵ₀ ≤ c ↔ ∀ n : ℕ, ↑n ≤ c :=
  ⟨fun h _ => (nat_lt_aleph0 _).le.trans h, fun h =>
    le_of_not_gt fun hn => by
      rcases lt_aleph0.1 hn with ⟨n, rfl⟩
      exact (Nat.lt_succ_self _).not_ge (Nat.cast_le.1 (h (n + 1)))⟩

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