Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.Icc_mk_mk

Modification history

2022-10-16 18:10
src/order/locally_finite.lean
feat(order/locally_finite): add lemmas expanding `finset.Icc` (#16996) …
Added prod.Icc_mk_mkView on Github →