Theorem Set.Finite.ecard_lt_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.Finite.ecard_lt_ecardView on Github →