PR #15412: feat(set_theory/cardinal/basic): `#α ≤ ℵ₀ ↔ co...

Stream: triage

[Random Issue Bot]

Today I chose PR 15412 for discussion!

feat(set_theory/cardinal/basic): #α ≤ ℵ₀ ↔ countable α
Created by @Violeta Hernández (@vihdzp) on 2022-07-16
Labels: WIP, awaiting-author, awaiting-CI

Is this PR still relevant? Any recent updates? Anyone making progress?