Theorem Set.ncard_iUnion_le_of_finite

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.ncard_iUnion_le_of_finiteView on Github →