Zulip Chat Archive
Stream: maths
Topic: empty set lemmas
Bernd Losert (Oct 15 2022 at 21:59):
Why don't we have iff for these two guys: set.nonempty.ne_empty and set.nonempty.not_subset_empty. I have s ≠ ∅ and now I can't simplify it.
Kyle Miller (Oct 15 2022 at 22:51):
Are you looking for docs#set.ne_empty_iff_nonempty?
Bernd Losert (Oct 16 2022 at 08:25):
Ah, it's in a different section. That was confusing. Thanks.
Last updated: May 02 2025 at 03:31 UTC