Commit 2025-10-02 19:28 3da1779e

View on Github →

feat(Order): synchronize IsAntichain API with IsChain (#29834) For IsAntichain, make empty/singleton two simp lemmas that exactly match the API in IsChain, and add an analogous isAntichain_union lemma. For IsChain, add a preimage lemma matching IsAntichain's and copy over a set of lemmas about different mappings preserving the predicate.

Estimated changes

Modified Mathlib/Order/Antichain.lean

deleted theorem isAntichain_singleton

added theorem isAntichain_union

Modified Mathlib/Order/Preorder/Chain.lean

added theorem IsChain.image_embedding

added theorem IsChain.image_embedding_iff

added theorem IsChain.image_iso

added theorem IsChain.image_iso_iff

added theorem IsChain.image_relEmbedding

added theorem IsChain.image_relEmbedding_iff

added theorem IsChain.image_relIso

added theorem IsChain.image_relIso_iff

added theorem IsChain.preimage

added theorem IsChain.preimage_embedding

added theorem IsChain.preimage_iso

added theorem IsChain.preimage_iso_iff

added theorem IsChain.preimage_relEmbedding

added theorem IsChain.preimage_relIso