Theorem Set.ecard_le_ecard

Modification history

2026-02-19 03:38

Mathlib/Data/Finite/Card.lean

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

Added Set.ecard_le_ecard View on Github →