Commit 2026-05-14 10:13 f181bae5

feat(SetTheory/Cardinal): IsStrongPrelimit predicate (#37406) We introduce a predicate for cardinals c such that x < c implies x < 2 ^ c. This is to IsStrongLimit as IsSuccPrelimit is to IsSuccLimit. We then make use of it in a few places where we were writing down ∀ x < c, x < 2 ^ c explicitly.