Theorem Cardinal.aleph0_lt_iff_aleph_one_le

Modification history

2026-02-25 00:49

Mathlib/SetTheory/Cardinal/Aleph.lean

feat(SetTheory/Cardinal): generalize infinite pigeonhole principle (#34091) …

Added Cardinal.aleph0_lt_iff_aleph_one_le View on Github →