Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-12 22:30 f6c8affd

View on Github →

feat(order/zorn) : chain_univ (#9162) univ is a r-chain iff r is trichotomous

Estimated changes

added theorem zorn.chain_univ_iff