finset.sum_union_inter mystery

Stream: new members

[Malvin Gattinger]

The documentation has https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html#finset.sum_union_inter but the mathlib sources itself do not :astonished:. The "source" link goes to finset.prod_union_inter instead.

In any case, I was actually searching for something without the interesection but then using ≤ instead of =. Is there something like the following? (And why does this fail due to a missing has_union (finset T)? Are there finsets where union does not exist? :thinking:

import data.finset.basic
import algebra.big_operators.order

lemma sum_union_le { T : Type } : ∀ { X Y : finset T } { F : T → ℕ }, (X ∪ Y).sum F ≤ X.sum F + Y.sum F :=
begin
  intros X Y F,
end