Theorem Cardinal.IsInaccessible.aleph0_lt

Modification history

2026-03-24 13:52
Mathlib/SetTheory/Cardinal/Regular.lean
chore(SetTheory/Cardinal/Regular): make `IsRegular` and `IsInaccessible` into structures (#36933) …
Deleted Cardinal.IsInaccessible.aleph0_ltView on Github →
2025-07-07 00:36
Mathlib/SetTheory/Cardinal/Regular.lean
refactor(SetTheory/Cardinal/Regular): review `IsInaccessible` API (#26606) …
Added Cardinal.IsInaccessible.aleph0_ltView on Github →