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 7b4616b commit c3bb38bCopy full SHA for c3bb38b
src/Std/Data/TreeSet/Lemmas.lean
@@ -589,8 +589,7 @@ theorem size_left_le_size_union [TransCmp cmp] : t₁.size ≤ (t₁ ∪ t₂).s
589
theorem size_right_le_size_union [TransCmp cmp] : t₂.size ≤ (t₁ ∪ t₂).size :=
590
DTreeMap.size_right_le_size_union
591
592
-theorem size_union_le_size_add_size [TransCmp cmp]
593
- :
+theorem size_union_le_size_add_size [TransCmp cmp] :
594
(t₁ ∪ t₂).size ≤ t₁.size + t₂.size :=
595
DTreeMap.size_union_le_size_add_size
596
0 commit comments