Commit 2025-12-03 20:10 11345931

feat(Order): replace the implementation of Set.chainHeight (#30345) Set.chainHeight is unused in Mathlib--it was a previous attempt to formalize heights for preorders before Order.height came into use. The current implementation Set.chainHeight is previously defined for Sets that had an LT order but it's behavior was unexpected for relations that were not strict orders, e.g. singleton sets with a reflexive relation would have infinite height. LE is such a relation so this implementation is very limited in what it could be used for. I replace it with an implementation that:

• Is defined for arbitrary relations instead of using [LT].
• Uses IsChain instead of List.IsChain for defining chains. This is equivalent for transitive relations, but behaves differently for non- transitive relations--it requires that all elements in the set are comparable instead of just comparability between neighboring elements in the List. This makes the definition better behaved for e.g. reflexive relations and better matches the definition of chain height typically used in the literature. The API has been slimmed down but what remains largely matches the previous API. Discussed on Zulip