Theorems · Definition · combinatorics
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).
- Defined in
- Mathlib.Order.SuccPred.Tree
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.ofPredproof · cited by 6,101
- IsAtomproof · cited by 130
- RootedTreestatement and proof · cited by 14
- SubRootedTreestatement and proof · cited by 10
- SubRootedTree.rootproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- SubRootedTree.root_ne_bot_of_mem_subtreesstatement and proof · cited by 2
- RootedTree.mem_subtrees_disjoint_iffstatement and proof · cited by 1
- RootedTree.subtrees_disjointstatement and proof · cited by 0
- RootedTree.subtreeOf_mem_subtreesstatement · cited by 0