Commit 2025-02-20 08:39 ff557b06

View on Github →

chore(SetTheory/Cardinal/Cofinality): make IsStrongLimit into a structure (#21971) This makes the definition more readable and gives us the projection lemmas automatically.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Cardinal.IsInaccessible.mk

deleted theorem Cardinal.IsStrongLimit.ne_zero

deleted theorem Cardinal.IsStrongLimit.two_power_lt

added structure Cardinal.IsStrongLimit

deleted def Cardinal.IsStrongLimit

modified theorem Cardinal.isStrongLimit_aleph0

modified theorem Cardinal.mk_bounded_subset

modified theorem Cardinal.mk_subset_mk_lt_cof