Commit 2022-06-06 10:35 0f5ea396

View on Github →

feat(order/antichain, order/minimal): some antichain lemmas (#14507) This PR adds a few lemmas about antichains, including their images under complementation and order isomorphisms.

Estimated changes

Modified src/order/antichain.lean

added theorem is_antichain.image_compl

added theorem is_antichain.image_embedding

added theorem is_antichain.image_embedding_iff

added theorem is_antichain.image_iso

added theorem is_antichain.image_iso_iff

added theorem is_antichain.image_rel_embedding

added theorem is_antichain.image_rel_embedding_iff

added theorem is_antichain.image_rel_iso

added theorem is_antichain.image_rel_iso_iff

added theorem is_antichain.preimage_compl

added theorem is_antichain.preimage_embedding

added theorem is_antichain.preimage_iso

added theorem is_antichain.preimage_iso_iff

added theorem is_antichain.preimage_rel_embedding

added theorem is_antichain.preimage_rel_iso

added theorem is_antichain.to_dual

added theorem is_antichain.to_dual_iff

Modified src/order/minimal.lean

added theorem is_antichain.max_lower_set_of

added theorem is_antichain.min_upper_set_of