Commit 2025-02-24 09:31 709c4284

View on Github →

feat(Data/Set/Card): a few missing lemmas (#22186) We add two simp lemmas where the RHS is Set.encard s and the LHS is something uglier. We also add two lemmas relating Set.Subsingleton and Set.Nontrivial with Set.encard.

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Card.lean

modified theorem Set.encard_inv

Modified Mathlib/Data/Set/Card.lean

added theorem Set.coe_fintypeCard

added theorem Set.encard_le_one_iff_subsingleton

added theorem Set.one_lt_encard_iff_nontrivial

added theorem Set.toENat_cardinalMk