Theorem Finset.exists_not_mem_of_card_lt_enatCard

Modification history

2025-09-23 05:58
Mathlib/Data/Set/Card.lean
feat(Data/Set/Card): every finset of card less than `ENat.card α` doesn't contain some element (#29900) …
Added Finset.exists_not_mem_of_card_lt_enatCardView on Github →