OAI/Combinatorics/ParityLifts/SparseTree.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ParityWL.Complexity.SparseTree line 7
2. def OAI.ParityWL.Complexity.SparseTree.root line 11
3. def OAI.ParityWL.Complexity.SparseTree.leaves line 15
4. def OAI.ParityWL.Complexity.SparseTree.nodes line 19
5. lemma OAI.ParityWL.Complexity.SparseTree.nodes_eq line 23
6. lemma OAI.ParityWL.Complexity.SparseTree.nodes_le line 28
7. def OAI.ParityWL.Complexity.SparseTree.Valid line 32
8. def OAI.ParityWL.Complexity.SparseTree.All line 37
9. lemma OAI.ParityWL.Complexity.sparse_tree_exists line 41