Commit 2022-12-24 19:17 41215b36

View on Github →

feat: port Order.Antichain (#1206)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Antichain.lean

added theorem IsAntichain.bot_mem_iff

added theorem IsAntichain.greatest_iff

added theorem IsAntichain.image

added theorem IsAntichain.image_compl

added theorem IsAntichain.image_embedding

added theorem IsAntichain.image_embedding_iff

added theorem IsAntichain.image_iso

added theorem IsAntichain.image_iso_iff

added theorem IsAntichain.image_relEmbedding

added theorem IsAntichain.image_relEmbedding_iff

added theorem IsAntichain.image_relIso

added theorem IsAntichain.image_relIso_iff

added theorem IsAntichain.insert_of_symmetric

added theorem IsAntichain.least_iff

added theorem IsAntichain.mono

added theorem IsAntichain.mono_on

added theorem IsAntichain.preimage

added theorem IsAntichain.preimage_compl

added theorem IsAntichain.preimage_embedding

added theorem IsAntichain.preimage_iso

added theorem IsAntichain.preimage_iso_iff

added theorem IsAntichain.preimage_relEmbedding

added theorem IsAntichain.preimage_relIso

added theorem IsAntichain.swap

added theorem IsAntichain.to_dual

added theorem IsAntichain.to_dual_iff

added theorem IsAntichain.top_mem_iff

added def IsAntichain

added theorem IsGreatest.antichain_iff

added theorem IsLeast.antichain_iff

added theorem IsStrongAntichain.eq

added theorem IsStrongAntichain.image

added theorem IsStrongAntichain.mono

added theorem IsStrongAntichain.preimage

added theorem IsStrongAntichain.swap

added def IsStrongAntichain

added def IsWeakAntichain

added theorem Set.Subsingleton.isAntichain

added theorem Set.Subsingleton.isStrongAntichain

added theorem Set.Subsingleton.isWeakAntichain

added theorem isAntichain_and_greatest_iff

added theorem isAntichain_and_least_iff

added theorem isAntichain_insert

added theorem isAntichain_insert_of_symmetric

added theorem isAntichain_singleton

added theorem isStrongAntichain_insert

added theorem isWeakAntichain_insert