Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ulower.down_up

Modification history

2020-05-07 22:43

src/data/equiv/encodable.lean

feat(data/equiv/encodable): `ulower` lowers countable types to `Type 0` (#2574) …

Added ulower.down_up View on Github →