Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonempty_ulift

Modification history

2021-12-15 19:58

src/logic/basic.lean

split(logic/nonempty): Split off `logic.basic` (#10762) …

Modified nonempty_ulift View on Github →

2017-12-14 21:29

logic/basic.lean

feat(logic/basic): add rewrite rules for nonempty

Added nonempty_ulift View on Github →