Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.Icc_eq

Modification history

2022-10-16 18:10

src/data/pi/interval.lean

feat(order/locally_finite): add lemmas expanding `finset.Icc` (#16996) …

Added pi.Icc_eq View on Github →