Commit 2024-02-29 00:55 efdfa67f

View on Github →

feat(Finset): add gcongr attributes (#9520)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.filter_singleton

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Lattice.lean

added theorem GCongr.finset_inf'_mono

added theorem GCongr.finset_sup'_le

Modified Mathlib/Order/Filter/AtTopBot.lean