Aronszajn trees

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

A κ-Aronszajn tree is a κ-tree such that there are no cofinal branch through the tree.

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

Uses 2 · Used by 2

Statement usesTree (set theory) · Level of a well-founded partial order

Used byAronszajn tree · \(\kappa\)-Suslin tree

DefinitionAronszajn tree#✓fully proved

An Aronszajn tree is a tree of height \(\aleph_1}\) all of whose levels are at most countable and which has no uncountable branches.

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

Uses 1

Statement uses\(\kappa\)-Aronszajn tree

Definition\(\omega_1\)-tree#✓fully proved

An ω₁-tree is a tree of height ω₁ all of whose levels are countable: every node has height < ω₁, every level Lev_α(T) with α < ω₁ is nonempty, and every such level is countable.

def IsOmega1Tree.{u} (α : Type u) [PartialOrder α] [WellFoundedLT α] : Prop :=
  IsTreeAt (aleph 1 : Cardinal.{u}) α

Uses 2

Statement usesTree (set theory) · Level of a well-founded partial order

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.