Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.card_Icc

Modification history

2021-12-26 03:49
src/data/pi/interval.lean
feat(data/pi/interval): Dependent functions to locally finite orders are locally finite (#11050) …
Added pi.card_IccView on Github →