We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 25a2051 commit d4210d5Copy full SHA for d4210d5
src/Std/Data/DTreeMap/Lemmas.lean
@@ -2279,7 +2279,7 @@ theorem mem_of_mem_union_of_not_mem_left [TransCmp cmp]
2279
/- Equiv -/
2280
theorem union_insert_right_equiv_union_insert [TransCmp cmp] {p : (a : α) × β a} :
2281
(t₁ ∪ (t₂.insert p.fst p.snd)).Equiv ((t₁ ∪ t₂).insert p.fst p.snd) :=
2282
- ⟨Impl.union_insert_right_equiv_insert_union t₁.wf t₂.wf⟩
+ ⟨Impl.union_insert_right_equiv_insert_union t₁.wf t₂.wf⟩
2283
2284
/- get? -/
2285
theorem get?_union [TransCmp cmp] [LawfulEqCmp cmp] {k : α} :
0 commit comments