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.
The unique atom less than an element in an OrderBot
with archimedean predecessor.
Equations
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
, whereinf
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.
Equations
- instCoeSortRootedTreeType = { coe := RootedTree.α }
A subtree is represented by its root, therefore this is a type synonym.
Equations
- SubRootedTree t = ↑t
The root of a SubRootedTree
.
The SubRootedTree
rooted at a given node.
Equations
- instSetLikeSubRootedTreeα t = { coe := fun (v : SubRootedTree t) => Set.Ici v.root, coe_injective' := ⋯ }
The coercion from a SubRootedTree
to a RootedTree
.
Equations
- ↑r = { α := ↑(Set.Ici r.root), semilatticeInf := Set.Ici.semilatticeInf, orderBot := Set.Ici.orderBot, predOrder := Set.OrdConnected.predOrder, isPredArchimedean := ⋯ }
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).
The immediate subtree of t
containing v
, or all of t
if v
is the root.
Equations
- t.subtreeOf v = t.subtree (IsPredArchimedean.findAtom v)