Skip to content

Commit dbd6020

Browse files
wkrozowskidatokrat
andauthored
Update src/Std/Data/TreeMap/Lemmas.lean
Co-authored-by: Paul Reichert <[email protected]>
1 parent 2f5028e commit dbd6020

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/Std/Data/TreeMap/Lemmas.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1642,7 +1642,6 @@ theorem getKey?_union [TransCmp cmp]
16421642
DTreeMap.getKey?_union
16431643

16441644
theorem getKey?_union_of_not_mem_left [TransCmp cmp]
1645-
16461645
{k : α} (not_mem : ¬k ∈ t₁) :
16471646
(t₁ ∪ t₂).getKey? k = t₂.getKey? k :=
16481647
DTreeMap.getKey?_union_of_not_mem_left not_mem

0 commit comments

Comments
 (0)