Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonempty.exists

Modification history

2021-12-15 19:58

src/logic/basic.lean

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

Modified nonempty.exists View on Github →

2021-10-20 01:45

src/logic/basic.lean

chore(*): remove uses of `universe variable` (#9794) …

Modified nonempty.exists View on Github →

2017-12-14 21:29

logic/basic.lean

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

Added nonempty.exists View on Github →