Theorem Set.Finite.ncard_biUnion_le

Modification history

2025-08-22 15:25
Mathlib/Data/Set/Card/Arithmetic.lean
feat(Data/Set/Card): add lemmas of the form `card_Union_le` (#28534) …
Added Set.Finite.ncard_biUnion_leView on Github →