Cardinality of union of finsets

Stream: Is there code for X?

[Stepan Nesterov]

Is there a lemma which states that the cardinality of a union of a collection of finsets (I am working with bUnion right now) is less than or equal to the sum of cardinalities of these finsets? I could only find lemmas about binary unions in data.finset.basic

[Ruben Van de Velde]

docs#finset.card_bUnion_le?

[Stepan Nesterov]

Ruben Van de Velde said:

docs#finset.card_bUnion_le?

Thanks!

[Kevin Buzzard]

Moral : guess the name of the lemma :-)