Commit 2025-07-07 00:36 b6a8f16b

View on Github →

refactor(SetTheory/Cardinal/Regular): review IsInaccessible API (#26606) This PR does the following:

Make the definition of IsInaccessible the more lightweight version.
Turn the old definition into a lemma isInaccessible_def.
Use dot notation wherever possible.
Add two extra convenience lemmas.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Regular.lean

added theorem Cardinal.IsInaccessible.aleph0_lt

added theorem Cardinal.IsInaccessible.isRegular

added theorem Cardinal.IsInaccessible.isStrongLimit

added theorem Cardinal.IsInaccessible.nat_lt

added theorem Cardinal.IsInaccessible.ne_zero

added theorem Cardinal.IsInaccessible.pos

added theorem Cardinal.IsInaccessible.univ

modified def Cardinal.IsInaccessible

added theorem Cardinal.isInaccesible_def

deleted theorem Cardinal.univ_inaccessible