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

• IsPredArchimedean.findAtom r = Order.pred^[Nat.find ⋯ - 1] r

@[simp]

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

@[simp]

theorem IsPredArchimedean.findAtom_bot {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] : IsPredArchimedean.findAtom ⊥ = ⊥

@[simp]

theorem IsPredArchimedean.pred_findAtom {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] (r : α) : Order.pred (IsPredArchimedean.findAtom r) = ⊥

@[simp]

theorem IsPredArchimedean.findAtom_eq_bot {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] {r : α} : IsPredArchimedean.findAtom r = ⊥ ↔ r = ⊥

theorem IsPredArchimedean.findAtom_ne_bot {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] {r : α} : IsPredArchimedean.findAtom r ≠ ⊥ ↔ r ≠ ⊥

theorem IsPredArchimedean.isAtom_findAtom {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] {r : α} (hr : r ≠ ⊥) : IsAtom (IsPredArchimedean.findAtom r)

@[simp]

theorem IsPredArchimedean.isAtom_findAtom_iff {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α] {r : α} : IsAtom (IsPredArchimedean.findAtom r) ↔ r ≠ ⊥

instance IsPredArchimedean.instIsAtomic {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] : IsAtomic α

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.

instance instCoeSortRootedTreeType : CoeSort RootedTree (Type u_2)

Equations

• instCoeSortRootedTreeType = { coe := RootedTree.α }

def SubRootedTree (t : RootedTree) : Type u_2

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

Equations

• SubRootedTree t = ↑t

def SubRootedTree.root {t : RootedTree} (v : SubRootedTree t) : ↑t

The root of a SubRootedTree.

Equations

• v.root = v

def RootedTree.subtree (t : RootedTree) (r : ↑t) : SubRootedTree t

The SubRootedTree rooted at a given node.

Equations

• t.subtree r = r

@[simp]

theorem RootedTree.root_subtree (t : RootedTree) (r : ↑t) : (t.subtree r).root = r

@[simp]

theorem RootedTree.subtree_root (t : RootedTree) (v : SubRootedTree t) : t.subtree v.root = v

theorem SubRootedTree.ext {t : RootedTree} {v₁ v₂ : SubRootedTree t} (h : v₁.root = v₂.root) : v₁ = v₂

instance instSetLikeSubRootedTreeα (t : RootedTree) : SetLike (SubRootedTree t) ↑t

Equations

• instSetLikeSubRootedTreeα t = { coe := fun (v : SubRootedTree t) => Set.Ici v.root, coe_injective' := ⋯ }

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) : RootedTree

The coercion from a SubRootedTree to a RootedTree.

Equations

• ↑r = RootedTree.mk ↑(Set.Ici r.root)

noncomputable instance instCoeOutSubRootedTreeRootedTree (t : RootedTree) : CoeOut (SubRootedTree t) RootedTree

Equations

• instCoeOutSubRootedTreeRootedTree t = { coe := SubRootedTree.coeTree }

@[simp]

theorem SubRootedTree.bot_mem_iff {t : RootedTree} (r : SubRootedTree t) : ⊥ ∈ r ↔ r.root = ⊥

def RootedTree.subtrees (t : RootedTree) : Set (SubRootedTree t)

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

• t.subtrees = {x : SubRootedTree t | IsAtom x.root}

theorem SubRootedTree.root_ne_bot_of_mem_subtrees {t : RootedTree} (r : SubRootedTree t) (hr : r ∈ t.subtrees) : r.root ≠ ⊥

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₂

theorem RootedTree.subtrees_disjoint {t : RootedTree} : t.subtrees.PairwiseDisjoint SetLike.coe

def RootedTree.subtreeOf (t : RootedTree) [DecidableEq ↑t] (v : ↑t) : SubRootedTree t

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)

@[simp]

theorem RootedTree.mem_subtreeOf {t : RootedTree} [DecidableEq ↑t] {v : ↑t} : v ∈ t.subtreeOf v

theorem RootedTree.subtreeOf_mem_subtrees {t : RootedTree} [DecidableEq ↑t] {v : ↑t} (hr : v ≠ ⊥) : t.subtreeOf v ∈ t.subtrees