Theorem Finset.dens_strictMono

Modification history

2026-05-11 06:34
Mathlib/Data/Finset/Density.lean
chore: untag duplicated `gcongr` lemmas (#38949) …
Modified Finset.dens_strictMonoView on Github →
2026-05-04 15:38
Mathlib/Data/Finset/Density.lean
chore: tag (almost) all `mono` lemmas as `@[gcongr]` (#38793) …
Modified Finset.dens_strictMonoView on Github →
2024-07-12 14:35
Mathlib/Data/Finset/Density.lean
feat: Density of a finset (#11243) …
Added Finset.dens_strictMonoView on Github →