Commit 2021-12-18 19:28 560f08f7

View on Github →

feat: more theorems on arrays and binary heaps (#138)

Estimated changes

Modified Mathlib/Data/Array/Basic.lean

added theorem Array.get?_eq_get

added theorem Array.get?_eq_get?

added theorem Array.get?_len_le

added theorem Array.get?_push_eq

added theorem Array.get?_push_lt

added theorem Array.get?_set

added theorem Array.get?_set_eq

added theorem Array.get?_set_ne

added theorem Array.get_eq_get

added theorem Array.get_push

Modified Mathlib/Data/BinaryHeap.lean

added def BinaryHeap.decreaseKey

added def BinaryHeap.get

added def BinaryHeap.increaseKey

added def BinaryHeap.insertExtractMax

added def BinaryHeap.replaceMax

added def BinaryHeap.singleton

added theorem BinaryHeap.size_pos_of_max