Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.comp_inf'_eq_inf'_comp

Modification history

2021-04-21 09:38
src/data/finset/lattice.lean
feat(data/finset/lattice): add `comp_sup'_eq_sup'_comp`, golf some proofs (#7275) …
Added finset.comp_inf'_eq_inf'_compView on Github →