Theorem Cardinal.not_isSuccLimit_of_lt_aleph0

Modification history

2024-09-18 06:51

Mathlib/SetTheory/Cardinal/Basic.lean

chore(SetTheory/Cardinal/Basic): `Cardinal.IsLimit` → `IsSuccLimit` (#16899)

Added Cardinal.not_isSuccLimit_of_lt_aleph0 View on Github →