Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.inf_univ_eq_infi

Modification history

2022-11-18 03:59
src/data/fintype/basic.lean
refactor(data/fintype/basic): split file (#17578)
Modified finset.inf_univ_eq_infiView 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.inf_univ_eq_infiView on Github →