Mathlib v3 is deprecated. Go to Mathlib v4

Theorem option.ne_none_iff_exists

Modification history

2020-09-27 05:22
src/data/option/basic.lean
chore(data/option): swap sides in `ne_none_iff_exists` (#4285) …
Modified option.ne_none_iff_existsView on Github →
2020-08-18 14:01
src/data/option/basic.lean
feat(data/option/basic): add ne_none_iff_exists (#3856)
Added option.ne_none_iff_existsView on Github →