Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 20:06 ad3e6672

View on Github →

feat(order/chain): Flags (#13089) Define the type of maximal chains, aka flags, of an order.

Estimated changes

added theorem flag.bot_mem
added theorem flag.chain_le
added theorem flag.chain_lt
added theorem flag.coe_mk
added theorem flag.ext
added theorem flag.mem_coe_iff
added theorem flag.mk_coe
added theorem flag.top_mem
added structure flag
added theorem is_max_chain.bot_mem
added theorem is_max_chain.top_mem