Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_true_iff_nonempty

Modification history

2021-12-15 19:58
src/logic/basic.lean
split(logic/nonempty): Split off `logic.basic` (#10762) …
Modified exists_true_iff_nonemptyView on Github →
2018-04-25 13:06
logic/basic.lean
feat(order): add liminf and limsup over filters (c.f. Sébastien Gouëzel's #115)
Added exists_true_iff_nonemptyView on Github →