Theorems · Definition · combinatorics
SubRootedTree
RootedTree → Type u_2
A subtree is represented by its root, therefore this is a type synonym.
- Defined in
- Mathlib.Order.SuccPred.Tree
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RootedTreestatement and proof · cited by 14
- RootedTree.αproof · cited by 10
Cited by15
Results whose statement or proof uses this declaration.
- SubRootedTree.rootstatement and proof · cited by 8
- RootedTree.subtreesstatement and proof · cited by 4
- SubRootedTree.extstatement and proof · cited by 2
- SubRootedTree.root_ne_bot_of_mem_subtreesstatement and proof · cited by 2
- RootedTree.subtreestatement · cited by 2
- RootedTree.subtreeOfstatement · cited by 2
- SubRootedTree.mem_iffstatement and proof · cited by 1
- RootedTree.mem_subtrees_disjoint_iffstatement and proof · cited by 1
- SubRootedTree.bot_mem_iffstatement and proof · cited by 0
- SubRootedTree.coeTreestatement and proof · cited by 0
- SubRootedTree.ext_iffstatement and proof · cited by 0
- RootedTree.mem_subtreeOfstatement · cited by 0