Clubs, stationary sets and normal ideals

DefinitionCountable subsets of a set#✓fully proved

[α]^ω or P_{ω₁}(α) is the set of countable subsets of α

def CountableSubsets.{u} (α : Type u) : Set (Set α) := {x | x.Countable}

Used by 1

Used byP-ideal dichotomy

StructureClub families of countable sets#✓fully proved

Let \(X\) be a set. A family \(C\) of subsets of \(X\) is club in the countable subsets of \(X\) when every member of \(C\) is countable (finite or countably infinite), every countable set \(x \subseteq X\) is contained in some member of \(C\), and for every sequence \(x_0 \subseteq x_1 \subseteq x_2 \subseteq \cdots\) of members of \(C\) the union \(\bigcup_{n \in \mathbb{N}} x_n\) belongs to \(C\).

structure IsClubOmega {α : Type*} (C : Set (Set α)) : Prop where
  mem_countable : ∀ x ∈ C, x.Countable
  cofinal : ∀ x : Set α, x.Countable → ∃ y ∈ C, x ⊆ y
  closed : ∀ f : ℕ → Set α, (∀ n, f n ∈ C) → Monotone f → (⋃ n, f n) ∈ C

Used by 2

Used byProper partial orders · Stationary families of countable sets

DefinitionStationary families of countable sets#✓fully proved

Let \(X\) be a set. A family \(S\) of subsets of \(X\) is stationary in the countable subsets of \(X\) when \(S\) meets every family \(C\) that is club in the countable subsets of \(X\), that is, some set belongs to both \(S\) and \(C\).

def IsStationaryOmega {α : Type*} (S : Set (Set α)) : Prop :=
  ∀ ⦃C : Set (Set α)⦄, IsClubOmega C → (S ∩ C).Nonempty

Uses 1

Statement usesClub families of countable sets

DefinitionClosure points of a finitary function#✓fully proved

Let \(X\) be a set and let \(F\) be a function assigning an element of \(X\) to every finite subset of \(X\). The closure points of \(F\) are the countable (finite or countably infinite) sets \(a \subseteq X\) such that \(F(s) \in a\) for every finite set \(s \subseteq a\).

def ClosurePoints {α : Type*} (F : Finset α → α) : Set (Set α) :=
  {x | x.Countable ∧ ∀ s : Finset α, ↑s ⊆ x → F s ∈ x}

Used by 1

Used byClosure points and clubs of countable subsets

DefinitionClosure points of a sequence of finitary functions#✓fully proved

Let \(X\) be a set and let \((F_n)_{n \in \mathbb{N}}\) be a sequence of functions, each assigning an element of \(X\) to every finite subset of \(X\). The closure points of \((F_n)\) are the countable (finite or countably infinite) sets \(x \subseteq X\) such that \(F_n(s) \in x\) for every \(n \in \mathbb{N}\) and every finite set \(s \subseteq x\).

def ClosurePointsSeq {α : Type*} (F : ℕ → Finset α → α) : Set (Set α) :=
  {x | x.Countable ∧ ∀ (n : ℕ) (s : Finset α), ↑s ⊆ x → F n s ∈ x}

Used by 1

Used byClosure points and clubs of countable subsets

TheoremClosure points and clubs of countable subsets#✓fully proved

1. Let F : Finset(α) → α. Then ClosurePointsSeq(λ n : ℕ,, F) = ClosurePoints(F). 2. For every finitary operation F, ∅ ∉ ClosurePoints(F). 3. Let f : ℕ → 𝒫(α) with each f(n) countable. Then ⋃_{n ∈ ℕ} f(n) is countable. 4. [α]^ω is club in [α]^ω. 5. ∅ is not stationary in [α]^ω. 6. If S is stationary in [α]^ω then S ≠ ∅. 7.

The full informal statement is in the module documentation directly above.

theorem closurePointsSeq_const.{u} {α : Type u} (F : Finset α → α) :
    ClosurePointsSeq (fun _ : ℕ => F) = ClosurePoints F

Uses 2

Statement usesClosure points of a finitary function · Closure points of a sequence of finitary functions

DefinitionSubsets of \(\lambda\) of size less than \(\kappa\)#✓fully proved

P_κ(λ) := { x ⊆ λ ∣ |x| < κ }

def powersetCardLT.{u} (κ lam : Cardinal.{u}) : Set (Set (Set.Iio lam.ord)) :=
  {x | #x < Cardinal.lift.{u+1} κ}

Used by 1

Used byClub subset of \(P_\kappa(\lambda)\)

StructureClub subset of \(P_\kappa(\lambda)\)#✓fully proved

C ⊆ P_κ(λ) is club iff

1. C is ⊆-cofinal: ∀ x ∈ P_κ(λ) ∃ y ∈ C (x ⊆ y), and
2. C is closed under unions of nonempty ⊆-directed subfamilies of size < κ: for every nonempty ⊆-directed D ⊆ C with |D| < κ, ⋃ D ∈ C.

structure IsClubPowersetCardLT.{u} (κ lam : Cardinal.{u})
    (C : Set (Set (Set.Iio lam.ord))) : Prop where
  subset : C ⊆ powersetCardLT κ lam
  cofinal : ∀ x ∈ powersetCardLT κ lam, ∃ y ∈ C, x ⊆ y
  closed : ∀ D : Set (Set (Set.Iio lam.ord)), D ⊆ C → D.Nonempty →
    #D < Cardinal.lift.{u+1} κ → DirectedOn (· ⊆ ·) D → (⋃₀ D) ∈ C

Uses 1

Statement usesSubsets of \(\lambda\) of size less than \(\kappa\)

DefinitionFamily containing all bounded subsets of a cardinal#✓fully proved

A set X⊆κ is bounded in κ if there is some β<κ with α<β for every α∈ X; equivalently, X⊆β for some β<κ.

A family I⊆𝒫(κ) contains all bounded sets if every bounded X⊆κ belongs to I:

∀ X ⊆ κ [ (∃ β < κ ∀ α ∈ X, α < β) ⟶ X ∈ I ].

def ContainsAllBounded.{u} (κ : Cardinal.{u}) (I : Set (Set (Set.Iio κ.ord))) : Prop :=
  ∀ X : Set (Set.Iio κ.ord),
    (∃ β : Set.Iio κ.ord, ∀ α ∈ X, (α : Ordinal) < (β : Ordinal)) → X ∈ I

Structure\(\kappa\)-complete ideal on a cardinal#✓fully proved

A κ-complete ideal on κ is a collection I ⊆ 𝒫(κ) such that:

1. ∅ ∈ I.
2. If A ∈ I and B ⊆ A, then B ∈ I.
3. κ ∉ I.
4. If λ < κ and ⟨ A_α : α < λ ⟩ is a sequence of members of I, then [ ⋃_{α < λ} A_α ∈ I. ]

structure IsKappaCompleteIdeal.{u} (κ : Cardinal.{u})
    (I : Set (Set (Set.Iio κ.ord))) : Prop where
  downward : ∀ X ∈ I, ∀ Y ⊆ X, Y ∈ I
  empty_mem : (∅ : Set (Set.Iio κ.ord)) ∈ I
  univ_not_mem : (Set.univ : Set (Set.Iio κ.ord)) ∉ I
  kappa_complete : ∀ F : Set (Set (Set.Iio κ.ord)),
    #F < Cardinal.lift.{u+1} κ → (∀ X ∈ F, X ∈ I) → ⋃₀ F ∈ I

DefinitionNormal ideal on a cardinal#✓fully proved

Let κ be a cardinal, identified with κ = Iio(κ.ord) = {α : Ordinal ∣ α < κ.ord}, and let I⊆𝒫(κ).

I is normal if it is closed under diagonal unions: for every κ-sequence ⟨ A_ξ : ξ<κ⟩ with A_ξ∈ I,

∇_{ξ<κ} A_ξ := {α<κ ∣ ∃ ξ<α, α∈ A_ξ} ∈ I.

Formally,

∀ A : κ → 𝒫(κ), (∀ ξ, A_ξ∈ I) → {α∈κ ∣ ∃ ξ∈κ, ξ<α ∧ α∈ A_ξ}∈ I.

def IsNormalIdeal.{u} (κ : Cardinal.{u}) (I : Set (Set (Set.Iio κ.ord))) : Prop :=
  ∀ (A : Set.Iio κ.ord → Set (Set.Iio κ.ord)),
    (∀ ξ, A ξ ∈ I) →
    {α : Set.Iio κ.ord | ∃ ξ : Set.Iio κ.ord, (ξ : Ordinal) < α ∧ α ∈ A ξ} ∈ I

DefinitionRegressive functions#✓fully proved

Let \(\kappa\) be a cardinal, identified with its initial ordinal, let \(S\) be a set of ordinals less than \(\kappa\), and let \(f\) be a function from \(S\) to the ordinals less than \(\kappa\). Then \(f\) is regressive if \(f(\alpha) < \alpha\) for every nonzero \(\alpha \in S\).

def IsRegressive (κ : Cardinal)
    (S : Set (Set.Iio κ.ord)) (f : ↥S → Set.Iio κ.ord) : Prop :=
  ∀ x : ↥S, (x : Ordinal) ≠ 0 → (f x : Ordinal) < (x : Ordinal)

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.