Commit 2026-02-19 03:38 4e3318d4

View on Github →

feat(Data/Finite/Card): Nat.card/ENat.card is strictly monotonic on finite sets (#34693)

Estimated changes

Modified Mathlib/Data/Finite/Card.lean

added theorem Set.Finite.card_strictMonoOn

added theorem Set.Finite.ecard_lt_ecard

added theorem Set.Finite.ecard_strictMonoOn

added theorem Set.card_strictMono

added theorem Set.ecard_le_ecard

added theorem Set.ecard_strictMono