diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-11 23:15:56 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-11 23:15:56 +0200 |
| commit | 9b79a910636735a706fdd9f015e0b47e3aa9a06a (patch) | |
| tree | e9699c18d503ebb9ba7ca05f36bea9a24df7862a /BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | |
| parent | 0086a3de4a8cc0f6c6390bcb951e0c7fb65d9034 (diff) | |
Continue heapRemoveLastWithIndexRelation.
Case for index equal removed index.
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index 726f5d7..e99617b 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -1,5 +1,5 @@ import BinaryHeap.CompleteTree.AdditionalOperations -import BinaryHeap.CompleteTree.Lemmas +import BinaryHeap.CompleteTree.AdditionalProofs.Get namespace BinaryHeap.CompleteTree.AdditionalProofs |