Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 09:46 43e7d1b5

View on Github →

feat(order/antichain): Antichains (#9926) This defines antichains mimicking the definition of chains.

Estimated changes

added theorem is_antichain.image
added theorem is_antichain.mk_max
added theorem is_antichain.mk_subset
added theorem is_antichain.mono
added theorem is_antichain.mono_on
added theorem is_antichain.preimage
added theorem is_antichain.swap
added def is_antichain
added theorem is_antichain_insert