Theoremsantisymm, bot_mem_iff, diff, empty, eq, eq', eq_setOf_maximal, eq_setOf_minimal, flip, greatest_iff, image, image_compl, image_embedding, image_embedding_iff, image_iso, image_iso_iff, image_relEmbedding, image_relEmbedding_iff, image_relIso, image_relIso_iff, insert, insert_of_symmetric, isAntisymm, isWeakAntichain, least_iff, maximal_mem_iff, minimal_mem_iff, mono, mono_on, not_lt, of_monotoneOn_strictAntiOn, of_strictMonoOn_antitoneOn, preimage, preimage_compl, preimage_embedding, preimage_iso, preimage_iso_iff, preimage_relEmbedding, preimage_relIso, singleton, subset, subsingleton, swap, to_dual, to_dual_iff, top_mem_iff, antichain_iff, antichain_iff, image, isAntichain, isEmpty_iff, nonempty_iff, eq, flip, image, insert, isAntichain, mono, preimage, subset, subsingleton, swap, eq, insert, subset, isAntichain, isStrongAntichain, isWeakAntichain, compl, inter_subsingleton_of_isAntichain_of_isChain, inter_subsingleton_of_isChain_of_isAntichain, isAntichain_and_greatest_iff, isAntichain_and_least_iff, isAntichain_coe_univ_iff, isAntichain_iff_forall_not_lt, isAntichain_insert, isAntichain_insert_of_symmetric, isAntichain_preimage_subtypeVal, isAntichain_union, isChain_and_isAntichain_iff_subsingleton, isStrongAntichain_insert, isWeakAntichain_insert, setOf_maximal_antichain, setOf_minimal_antichain, subsingleton_of_isChain_of_isAntichain | 85 |