Theorem GCongr.finset_inf'_mono

Modification history

2024-07-31 19:18
Mathlib/Data/Finset/Lattice.lean
feat: gcongr works with eta and proofs (#15364) …
Deleted GCongr.finset_inf'_monoView on Github →
2024-02-29 00:55
Mathlib/Data/Finset/Lattice.lean
feat(Finset): add `gcongr` attributes (#9520)
Added GCongr.finset_inf'_monoView on Github →