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 0371fb3 commit e1736e9Copy full SHA for e1736e9
src/Std/Data/TreeMap/Lemmas.lean
@@ -1712,8 +1712,7 @@ theorem size_left_le_size_union [TransCmp cmp] : t₁.size ≤ (t₁ ∪ t₂).s
1712
theorem size_right_le_size_union [TransCmp cmp] : t₂.size ≤ (t₁ ∪ t₂).size :=
1713
DTreeMap.size_right_le_size_union
1714
1715
-theorem size_union_le_size_add_size [TransCmp cmp]
1716
- :
+theorem size_union_le_size_add_size [TransCmp cmp] :
1717
(t₁ ∪ t₂).size ≤ t₁.size + t₂.size :=
1718
DTreeMap.size_union_le_size_add_size
1719
0 commit comments