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