Theorem Set.Finite.card_strictMonoOn

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.card_strictMonoOnView on Github →