Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-07 00:44 69e07e25

View on Github →

chore(order/zorn): add docstrings, drop chain.directed (#1861) chain.directed_on is almost the same and uses a named predicate.

Estimated changes

deleted theorem zorn.chain.directed
modified def zorn.succ_chain
modified def zorn.super_chain