Lemmas

📁 Source: Batteries/Data/BinomialHeap/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems size_eq, deleteMin_fst, findMin_val, realSize_eq	4
Total	4

Batteries.BinomialHeap.Imp.Heap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deleteMin_fst 📖	mathematical	—	Batteries.BinomialHeap.Imp.Heap deleteMin head?	—	findMin_val
findMin_val 📖	mathematical	—	Batteries.BinomialHeap.Imp.FindMin.val findMin headD	—	findMin.eq_2 headD.eq_2

Batteries.BinomialHeap.Imp.Heap.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
size_eq 📖	mathematical	Batteries.BinomialHeap.Imp.Heap.WF	Batteries.BinomialHeap.Imp.Heap.size Batteries.BinomialHeap.Imp.Heap.realSize	—	Batteries.BinomialHeap.Imp.HeapNode.WF.realSize_eq

Batteries.BinomialHeap.Imp.HeapNode.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realSize_eq 📖	mathematical	Batteries.BinomialHeap.Imp.HeapNode.WF	Batteries.BinomialHeap.Imp.HeapNode.realSize	—	Batteries.BinomialHeap.Imp.HeapNode.realSize.eq_2

---

← Back to Index