Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.sup_univ_eq_supr

Modification history

2022-11-18 03:59
src/data/fintype/basic.lean
refactor(data/fintype/basic): split file (#17578)
Modified finset.sup_univ_eq_suprView on Github →
2021-07-26 07:37
src/data/fintype/basic.lean
feat(data/fintype/basic): add `finset.(sup|inf)_univ_eq_(supr|infi)` (#8397)
Added finset.sup_univ_eq_suprView on Github →