Basic
📁 Source: PhysLean/Mathematics/DataStructures/FourTree/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsFourTree, Branch, card, mem, Leaf, mem, Trunk, card, mem, Twig, card, mem, card, fromMultiset, instDecidableEqLeaf, decEq, instDecidableMemOfDecidableEq, instDecidableMemOfDecidableEq_1, instDecidableMemOfDecidableEq_2, instDecidableMemOfDecidableEq_3, instDecidableMemOfDecidableEq_4, instDecidableMemProdOfDecidableEq, instMembershipProd, instRepr, instReprBranch, instReprLeaf, instReprTrunk, instReprTwig, mem, toMultiset | 30 |
| 3 | |
| Total | 33 |
PhysLean
Definitions
| Name | Category | Theorems |
|---|---|---|
FourTree 📖 | CompData |
PhysLean.FourTree
Definitions
| Name | Category | Theorems |
|---|---|---|
Branch 📖 | CompData | — |
Leaf 📖 | CompData | — |
Trunk 📖 | CompData | — |
Twig 📖 | CompData | — |
card 📖 | CompOp | |
fromMultiset 📖 | CompOp | — |
instDecidableEqLeaf 📖 | CompOp | — |
instDecidableMemOfDecidableEq 📖 | CompOp | — |
instDecidableMemOfDecidableEq_1 📖 | CompOp | — |
instDecidableMemOfDecidableEq_2 📖 | CompOp | — |
instDecidableMemOfDecidableEq_3 📖 | CompOp | — |
instDecidableMemOfDecidableEq_4 📖 | CompOp | — |
instDecidableMemProdOfDecidableEq 📖 | CompOp | — |
instMembershipProd 📖 | CompOp | |
instRepr 📖 | CompOp | — |
instReprBranch 📖 | CompOp | — |
instReprLeaf 📖 | CompOp | — |
instReprTrunk 📖 | CompOp | — |
instReprTwig 📖 | CompOp | — |
mem 📖 | MathDef | — |
toMultiset 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
card_eq_toMultiset_card 📖 | mathematical | — | cardtoMultiset | — | — |
mem_iff_mem_toMultiset 📖 | mathematical | — | PhysLean.FourTreeinstMembershipProdtoMultiset | — | — |
mem_of_parts 📖 | mathematical | TrunkBranchTwigLeaf | PhysLean.FourTreeinstMembershipProd | — | mem_iff_mem_toMultiset |
PhysLean.FourTree.Branch
Definitions
| Name | Category | Theorems |
|---|---|---|
card 📖 | CompOp | — |
mem 📖 | MathDef | — |
PhysLean.FourTree.Leaf
Definitions
| Name | Category | Theorems |
|---|---|---|
mem 📖 | MathDef | — |
PhysLean.FourTree.Trunk
Definitions
| Name | Category | Theorems |
|---|---|---|
card 📖 | CompOp | — |
mem 📖 | MathDef | — |
PhysLean.FourTree.Twig
Definitions
| Name | Category | Theorems |
|---|---|---|
card 📖 | CompOp | — |
mem 📖 | MathDef | — |
PhysLean.FourTree.instDecidableEqLeaf
Definitions
| Name | Category | Theorems |
|---|---|---|
decEq 📖 | CompOp | — |
---