Zulip Chat Archive
Stream: Is there code for X?
Topic: is_empty ↥s
Violeta Hernández (Jun 24 2022 at 04:43):
Do we have is_empty ↥s ↔ s = Ø?
Junyan Xu (Jun 24 2022 at 05:34):
Only the contrapositives exist, it seems: docs#finset.nonempty_coe_sort, docs#set.nonempty_coe_sort
Junyan Xu (Jun 24 2022 at 05:36):
the only if direction exists for sets: docs#set.has_emptyc.emptyc.is_empty
Last updated: May 02 2025 at 03:31 UTC