Theorem Cardinal.fact_isRegular_aleph0

Modification history

2025-03-11 00:25

Mathlib/SetTheory/Cardinal/Cofinality.lean

chore(SetTheory/Cardinal/Cofinality): split file (#21972) …

Modified Cardinal.fact_isRegular_aleph0 View on Github →

2025-01-23 06:28

Mathlib/SetTheory/Cardinal/Cofinality.lean

feat(CategoryTheory): `κ`-filtered categories (#20005) …

Added Cardinal.fact_isRegular_aleph0 View on Github →