theorem
Batteries.BinomialHeap.Imp.Heap.findMin_val
{α : Type u_1}
{s : Batteries.BinomialHeap.Imp.Heap α}
{le : α → α → Bool}
{k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α}
{res : Batteries.BinomialHeap.Imp.FindMin α}
:
(Batteries.BinomialHeap.Imp.Heap.findMin le k s res).val = Batteries.BinomialHeap.Imp.Heap.headD le res.val s
theorem
Batteries.BinomialHeap.Imp.Heap.deleteMin_fst
{α : Type u_1}
{s : Batteries.BinomialHeap.Imp.Heap α}
{le : α → α → Bool}
:
Option.map (fun (x : α × Batteries.BinomialHeap.Imp.Heap α) => x.fst) (Batteries.BinomialHeap.Imp.Heap.deleteMin le s) = Batteries.BinomialHeap.Imp.Heap.head? le s
@[simp]
theorem
Batteries.BinomialHeap.Imp.HeapNode.WF.realSize_eq
{α : Type u_1}
{le : α → α → Bool}
{a : α}
{n : Nat}
{s : Batteries.BinomialHeap.Imp.HeapNode α}
:
Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → s.realSize + 1 = 2 ^ n
@[simp]
theorem
Batteries.BinomialHeap.Imp.Heap.WF.size_eq
{α : Type u_1}
{le : α → α → Bool}
{n : Nat}
{s : Batteries.BinomialHeap.Imp.Heap α}
:
Batteries.BinomialHeap.Imp.Heap.WF le n s → s.size = s.realSize