Theorems · Theorem · combinatorics
BinaryTree.mem_treesOfNumNodesEq
∀ {x : BinaryTree Unit} {n : ℕ}, x ∈ BinaryTree.treesOfNumNodesEq n ↔ x.numNodes = n- Cited by
- 1 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- BinaryTreestatement and proof · cited by 41
- BinaryTree.numNodesstatement and proof · cited by 11
- BinaryTree.treesOfNumNodesEqstatement and proof · cited by 10
- BinaryTree.treesOfNumNodesEq_succproof · cited by 2
- BinaryTree.treesOfNumNodesEq_zeroproof · cited by 2
- BinaryTree.node.injEqproof · cited by 1
- BinaryTree.ctorIdxproof · cited by 1
- BinaryTree.unitRecOnproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- BinaryTree.mem_treesOfNumNodesEq_numNodesproof · cited by 0