Commit 2025-03-06 22:04 3fcade7c

View on Github →

chore(SetTheory/Cardinal/Basic): move IsStrongLimit (#19723) This definition doesn't rely on cofinality in any way.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.isStrongLimit_beth

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.IsStrongLimit.aleph0_le

added theorem Cardinal.IsStrongLimit.isLimit

added structure Cardinal.IsStrongLimit

added theorem Cardinal.isStrongLimit_aleph0

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

deleted theorem Cardinal.IsStrongLimit.aleph0_le

deleted theorem Cardinal.IsStrongLimit.isLimit

deleted structure Cardinal.IsStrongLimit

deleted theorem Cardinal.isStrongLimit_aleph0

deleted theorem Cardinal.isStrongLimit_beth