Function lemma_flatten_cardinality_under_disjointness Copy item path

pairwise_disjoint(parts),

parts.flatten().len() == parts.fold(0nat, |acc: nat, p: Set<A>| acc + p.len()),

If parts is a finite set of finite, pairwise-disjoint sets, then the cardinality of the union is the sum of cardinalities.