Theorem Set.Finite.ncard_strictMonoOn

Modification history

2026-07-17 09:57

Mathlib/Data/Set/Card.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Modified Set.Finite.ncard_strictMonoOn View on Github →

2026-02-02 00:53

Mathlib/Data/Set/Card.lean

feat(Data/Set/Card): `ncard`/`encard` is strictly monotonic on finite sets (#34689)

Added Set.Finite.ncard_strictMonoOn View on Github →