Commit 2026-03-31 08:08 96c77b07
View on Github →feat: simplify ℵ₁ ≤ c to ℵ₀ < c (#37024)
We simplify c < ℵ₁ to c ≤ ℵ₀ and ℵ₁ ≤ c to ℵ₀ < c, under the logic that there is more to be said about ℵ₀ (the least infinite cardinal, etc.) than there is about ℵ₁, characterized only by being the successor to ℵ₀.