Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 06:04 c1f8ac50

View on Github →

feat(order/zorn): add Zorn lemma on a preorder (#13803)

Estimated changes

Modified src/order/chain.lean

added theorem is_chain.mono_rel

Modified src/order/zorn.lean

modified theorem zorn_nonempty_partial_order

added theorem zorn_nonempty_preorder

added theorem zorn_nonempty_preorder₀

modified theorem zorn_partial_order

modified theorem zorn_partial_order₀

added theorem zorn_preorder

added theorem zorn_preorder₀