Mathlib v3 is deprecated. Go to Mathlib v4

Theorem option.subsingleton_iff_is_empty

Modification history

2021-08-14 11:55
src/logic/unique.lean
chore(data/option,data/set): a few lemmas, golf (#8636) …
Added option.subsingleton_iff_is_emptyView on Github →