Theorem Cardinal.lt_aleph_one_iff

Modification history

2026-03-31 08:08
Mathlib/SetTheory/Cardinal/Aleph.lean
feat: simplify ℵ₁ ≤ c to ℵ₀ < c (#37024) …
Added Cardinal.lt_aleph_one_iffView on Github →