Documentation Verification Report

UniqueMap

📁 Source: PhysLean/Mathematics/DataStructures/FourTree/UniqueMap.lean

Statistics

Metric	Count
Definitions `uniqueMap3`, `uniqueMap4`, `uniqueMap4`, `uniqueMap3`, `uniqueMap4`, `uniqueMap3`, `uniqueMap4`, `uniqueMap3`, `uniqueMap4`	9
Theorems `exists_of_mem_uniqueMap3`, `exists_of_mem_uniqueMap4`, `map_mem_uniqueMap3`, `map_mem_uniqueMap4`	4
Total	13

PhysLean.FourTree

Definitions

Name	Category	Theorems
`uniqueMap3` 📖	CompOp	1 math math: `map_mem_uniqueMap3`
`uniqueMap4` 📖	CompOp	1 math math: `map_mem_uniqueMap4`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_mem_uniqueMap3` 📖	—	`PhysLean.FourTree` `instMembershipProd` `uniqueMap3`	—	—	`mem_iff_mem_toMultiset` `mem_of_parts`
`exists_of_mem_uniqueMap4` 📖	—	`PhysLean.FourTree` `instMembershipProd` `uniqueMap4`	—	—	`mem_iff_mem_toMultiset` `mem_of_parts`
`map_mem_uniqueMap3` 📖	mathematical	`PhysLean.FourTree` `instMembershipProd`	`uniqueMap3`	—	`mem_iff_mem_toMultiset`
`map_mem_uniqueMap4` 📖	mathematical	`PhysLean.FourTree` `instMembershipProd`	`uniqueMap4`	—	`mem_iff_mem_toMultiset`

PhysLean.FourTree.Branch

Definitions

Name	Category	Theorems
`uniqueMap3` 📖	CompOp	—
`uniqueMap4` 📖	CompOp	—

PhysLean.FourTree.Leaf

Definitions

Name	Category	Theorems
`uniqueMap4` 📖	CompOp	—

PhysLean.FourTree.Trunk

Definitions

Name	Category	Theorems
`uniqueMap3` 📖	CompOp	—
`uniqueMap4` 📖	CompOp	—

PhysLean.FourTree.Twig

Definitions

Name	Category	Theorems
`uniqueMap3` 📖	CompOp	—
`uniqueMap4` 📖	CompOp	—

---

← Back to Index