Mathlib Changelog
v3
Changelog
About
Github
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
Modified
src/data/set/pairwise.lean
added
theorem
reflexive.set_pairwise_iff
added
theorem
set.pairwise_iff_of_refl
Modified
src/order/chain.lean
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