Suslin trees

Definition\(\kappa\)-Suslin tree#✓fully proved

A κ-Suslin tree is a κ-Aronszajn tree with no antichains of size κ.

def IsSuslinTreeAt.{u} (κ : Cardinal.{u}) (α : Type u) [PartialOrder α] [WellFoundedLT α] : Prop :=
    IsAronszajnTreeAt κ α ∧ ∀ A : Set α, IsAntichain (· ≤ ·) A → #A < κ

Uses 1 · Used by 1

Statement uses\(\kappa\)-Aronszajn tree

Used bySuslin tree

DefinitionSuslin tree#✓fully proved

A Suslin tree is a tree of height \(\aleph_1}\) with no uncountable branches and no uncountable antichains.

def IsSuslinTree.{u} (α : Type u) [PartialOrder α] [WellFoundedLT α] : Prop :=
  IsSuslinTreeAt (aleph 1) α

Uses 1

Statement uses\(\kappa\)-Suslin tree

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.