Commit 2022-12-29 00:36 422debc7

View on Github →

feat: port Order.Chain (#1205) I also fixed a typo I did in my own name in a previous PR, thanks Yury for catching it :)

Estimated changes

added theorem ChainClosure.isChain
added theorem ChainClosure.total
added inductive ChainClosure
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 IsChain.directedOn
added theorem IsChain.exists3
added theorem IsChain.image
added theorem IsChain.insert
added theorem IsChain.mono
added theorem IsChain.mono_rel
added theorem IsChain.succ
added theorem IsChain.symm
added theorem IsChain.total
added def IsChain
added theorem IsMaxChain.bot_mem
added theorem IsMaxChain.isChain
added theorem IsMaxChain.top_mem
added def IsMaxChain
added def SuccChain
added def SuperChain
added theorem chainClosure_empty
added theorem chainClosure_maxChain
added theorem isChain_empty
added theorem isChain_univ_iff
added def maxChain
added theorem maxChain_spec
added theorem subset_succChain
added theorem succChain_spec