Commit 2025-09-23 05:58 5d37eb68

View on Github →

feat(Data/Set/Card): every finset of card less than ENat.card α doesn't contain some element (#29900) From the ProofBench workshop

Estimated changes

Modified Mathlib/Data/Set/Card.lean

added theorem Finset.exists_not_mem_of_card_lt_enatCard

modified theorem Function.Embedding.encard_le

modified theorem Set.encard_congr

modified theorem Set.encard_univ

modified theorem Set.encard_univ_coe

Modified Mathlib/MeasureTheory/Measure/Count.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem ENat.card_le_card_of_injective

added theorem ENat.card_le_one

added theorem ENat.card_pos

added theorem ENat.one_lt_card