Infinitary combinatorics

Combinatorics of infinite and uncountable sets: clubs and stationary sets, partition relations, Δ-systems, almost disjoint families, combinatorial principles such as diamond and square, set-theoretic trees, Ramsey ultrafilters and the structure of P(ω)/fin.

• Almost disjoint families
• Aronszajn, Suslin and special trees
• Automorphisms of P(ω)/fin
• Clubs, stationary sets and normal ideals
• Diamond principle
• Partition calculus
• Square principle

DefinitionRamsey ultrafilter#✓fully proved

An ultrafilter \(U\) on \(\mathbb{N}\) is Ramsey if for every sequence \((A_n)_{n \in \mathbb{N}}\) of pairwise disjoint subsets of \(\mathbb{N}\) whose union is \(\mathbb{N}\) and such that \(A_n \notin U\) for all \(n\), there is \(X \in U\) such that \(X \cap A_n\) has at most one element for every \(n\).

def IsRamseyUltrafilter (U : Ultrafilter ℕ) : Prop :=
  ∀ A : ℕ → Set ℕ, Pairwise (Disjoint on A) → (⋃ n, A n) = univ → (∀ n, A n ∉ U) →
    ∃ X ∈ U, ∀ n, (X ∩ A n).Subsingleton

DefinitionΔ-system#✓fully proved

A family \(A\) of subsets of a type \(\alpha\) is a Δ-system with root \(r \subseteq \alpha\) if \(s \cap t = r\) for any two distinct members \(s\) and \(t\) of \(A\).

def IsDeltaSystem {α : Type*} (A : Set (Set α)) (r : Set α) : Prop :=
    A.Pairwise fun s t => s ∩ t = r

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.