diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-28 10:41:37 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-28 10:41:37 +0200 |
| commit | 5ed262b0fcbc37c162bc657b8f3a6d4214bbbb5e (patch) | |
| tree | f7519cc16ea08afbd23e5bf9ba10ffdde9767bca /BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | |
| parent | b1821bdf7fb928be27a9919f4969883a2f6670ff (diff) | |
Remove redundant contains_iff_index_exists' function.
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index 7a0c893..950183b 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -82,14 +82,10 @@ private theorem if_contains_get_eq {α : Type u} {n : Nat} (tree : CompleteTree assumption -theorem contains_iff_index_exists' {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := by +theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := by constructor case mpr => simp only [forall_exists_index] exact if_get_eq_contains tree element case mp => exact if_contains_get_eq tree element - -theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (_ : n > 0): tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := - match n, tree with - | _+1, tree => contains_iff_index_exists' tree element |