Documentation

Mathlib.Order.SuccPred.Tree

Rooted trees #

This file proves basic results about rooted trees, represented using the ancestorship order. This is a PartialOrder, with PredOrder with the immediate parent as a predecessor, and an OrderBot which is the root. We also have an IsPredArchimedean assumption to prevent infinite dangling chains.

def IsPredArchimedean.findAtom {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] (r : α) :
α

The unique atom less than an element in an OrderBot with archimedean predecessor.

Equations
@[simp]
structure RootedTree :
Type (u_2 + 1)

The type of rooted trees.

  • α : Type u_2

    The type representing the elements in the tree.

  • semilatticeInf : SemilatticeInf self

    The type should be a SemilatticeInf, where inf is the least common ancestor in the tree.

  • orderBot : OrderBot self

    The type should have a bottom, the root.

  • predOrder : PredOrder self

    The type should have a predecessor for every element, its parent.

  • isPredArchimedean : IsPredArchimedean self

    The predecessor relationship should be archimedean.

A subtree is represented by its root, therefore this is a type synonym.

Equations

The root of a SubRootedTree.

Equations

The SubRootedTree rooted at a given node.

Equations
@[simp]
theorem RootedTree.root_subtree (t : RootedTree) (r : t) :
(t.subtree r).root = r
theorem SubRootedTree.ext {t : RootedTree} {v₁ v₂ : SubRootedTree t} (h : v₁.root = v₂.root) :
v₁ = v₂
theorem SubRootedTree.ext_iff {t : RootedTree} {v₁ v₂ : SubRootedTree t} :
v₁ = v₂ v₁.root = v₂.root
Equations
theorem SubRootedTree.mem_iff {t : RootedTree} {r : SubRootedTree t} {v : t} :
v r r.root v
@[reducible]
noncomputable def SubRootedTree.coeTree {t : RootedTree} (r : SubRootedTree t) :

The coercion from a SubRootedTree to a RootedTree.

Equations

All of the immediate subtrees of a given rooted tree, that is subtrees which are rooted at a direct child of the root (or, order theoretically, at an atom).

Equations
theorem RootedTree.mem_subtrees_disjoint_iff {t : RootedTree} {t₁ t₂ : SubRootedTree t} (ht₁ : t₁ t.subtrees) (ht₂ : t₂ t.subtrees) (v₁ v₂ : t) (h₁ : v₁ t₁) (h₂ : v₂ t₂) :
Disjoint v₁ v₂ t₁ t₂

The immediate subtree of t containing v, or all of t if v is the root.

Equations
@[simp]
theorem RootedTree.mem_subtreeOf {t : RootedTree} [DecidableEq t] {v : t} :