Trees in set theory

DefinitionTree (set theory)#✓fully proved

A tree is a partially ordered set (T, <) iwith the property that for each x ∈ T, the set { y ∈ T : y < x } of all predecessors of x is well-ordered by <).

def IsTree.{u} (α : Type u) [PartialOrder α] [WellFoundedLT α] : Prop :=
  ∀ x : α, IsChain (· ≤ ·) {y : α | y < x}

Used by 3

Used by\(\kappa\)-Aronszajn tree · \(\omega_1\)-tree · Normal tree at a cardinal

DefinitionLevel of a well-founded partial order#✓fully proved

For an ordinal α, the α-th level of a well-founded partial order (T, <) is Lev_α(T) = { x ∈ T : ht(x) = α }, the set of elements whose height equals α.

def level.{u} (α : Type u) [PartialOrder α] [WellFoundedLT α] (a : Ordinal.{u}) : Set α :=
  {x : α | WellFounded.rank (· < ·) x = a}

Used by 3

Used by\(\kappa\)-Aronszajn tree · \(\omega_1\)-tree · Normal tree at a cardinal

DefinitionNormal tree at a cardinal#✓fully proved

Let κ be a cardinal and (α,≤) a well-founded partial order; for x∈α let rank(x) denote the rank of x in the well-founded relation <. α is a normal tree at κ if:

\[\begin{enumerate} \item $\alpha$ is a tree at $\kappa$, i.e. \begin{itemize} \item $\forall x\in\alpha$, $\{y \mid y\lt x\}$ is a chain, \item $\forall x\in\alpha,\ \exists a\lt \kappa.\mathrm{ord},\ x\in\mathrm{level}_\alpha(a)$, \item $\forall a\lt \kappa.\mathrm{ord},\ \mathrm{level}_\alpha(a)\neq\emptyset$ and $|\mathrm{level}_\alpha(a)|\lt \kappa$; \end{itemize} \item $\alpha$ has a root: $\exists r\in\alpha\ \forall x\in\alpha,\ r\le x$; \item every node can be extended to any higher level below $\kappa$: \[ \forall x\in\alpha\ \forall b\lt \kappa.\mathrm{ord}\; \bigl(\operatorname{rank}(x)\lt b \to \exists y\in\alpha\ (x\lt y \land \operatorname{rank}(y)=b)\bigr); \] \item every node splits: \[ \forall x\in\alpha\ \exists y,z\in\alpha\; \bigl(x\lt y \land x\lt z \land y\not\le z \land z\not\le y\bigr). \] \end{enumerate}\]

def IsNormalTreeAt.{u} (κ : Cardinal.{u}) (α : Type u) [PartialOrder α] [WellFoundedLT α] : Prop :=
  IsTreeAt κ α ∧
  (∃ r : α, ∀ x : α, r ≤ x) ∧
  (∀ x : α, ∀ b : Ordinal.{u},
      WellFounded.rank (· < ·) x < b → b < κ.ord →
      ∃ y : α, x < y ∧ WellFounded.rank (· < ·) y = b) ∧
  (∀ x : α, ∃ y z : α, x < y ∧ x < z ∧ ¬ (y ≤ z) ∧ ¬ (z ≤ y))

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.