Mahlo cardinals
DefinitionMahlo cardinal#✓fully proved
MetaMathlibExt.IsMahlo
A cardinal κ is Mahlo if κ is inaccessible and the set { λ < κ : λ is inaccessible } of inaccessibles below κ is stationary in κ.
def IsMahlo.{u} (κ : Cardinal.{u}) : Prop :=
Cardinal.IsInaccessible κ ∧ IsStationary (inaccessibleBelow κ)def inaccessibleBelow.{u} (κ : Cardinal.{u}) : Set (Set.Iio κ.ord) :=
{α | Cardinal.IsInaccessible α.val.card ∧ α.val.card.ord = α.val}MathlibExt/SetTheory/Cardinal/LargeCardinal/Inaccessible.lean:67
Uses 1
Statement usesSet of inaccessible cardinals below a cardinal
DefinitionWeakly Mahlo cardinal#✓fully proved
MetaMathlibExt.IsWeaklyMahlo
A cardinal κ is weakly Mahlo if κ is weakly inaccessible and { λ < κ : λ is a regular cardinal } is stationary in κ.
def IsWeaklyMahlo.{u} (κ : Cardinal.{u}) : Prop :=
IsWeaklyInaccessible κ ∧
IsStationary {α : Set.Iio κ.ord | (α.val.card).IsRegular ∧ α.val.card.ord = α.val}def IsWeaklyInaccessible.{u} (κ : Cardinal.{u}) : Prop :=
ℵ₀ < κ ∧ κ.IsRegular ∧ Order.IsSuccLimit κMathlibExt/SetTheory/Cardinal/LargeCardinal/Inaccessible.lean:61
Uses 1
Statement usesWeakly inaccessible cardinal
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.