Commit 2025-04-05 18:24 6f40e886

View on Github →

chore(Order/Minimal): don't import CompleteLattice (#23592) Achieve this by:

  • splitting Order.Chain into Order.CompleteLattice.Chain for the material requiring CompleteLattice and Order.Preorder.Chain for the rest.
  • turning an import around between Order.Minimal and Order.UpperLower.Closure

Estimated changes

added theorem ChainClosure.isChain
added theorem ChainClosure.total
added inductive ChainClosure
added theorem chainClosure_empty
added theorem chainClosure_maxChain
added def maxChain
added theorem maxChain_spec
deleted theorem ChainClosure.isChain
deleted theorem ChainClosure.total
deleted inductive ChainClosure
deleted theorem chainClosure_empty
deleted theorem chainClosure_maxChain
deleted def maxChain
deleted theorem maxChain_spec