mathlib
84f4d5cc - feat(order/zorn): nonempty formulation of Zorn's lemma (#6532)

Commit

4 years ago

feat(order/zorn): nonempty formulation of Zorn's lemma (#6532) In practice it's often helpful to have this alternate formulation of Zorn's lemma

Author

b-mehta

Parents