Commit 2021-04-26 18:22 a5cb13a6

View on Github →

feat(order/zorn): upward inclusion variant of Zorn's lemma (#7362) add zorn_superset This also add various missing bits of whitespace throughout the file.

Estimated changes

Modified src/order/zorn.lean

modified theorem zorn.chain.directed_on

modified theorem zorn.chain.image

modified theorem zorn.chain.mono

added theorem zorn.chain.symm

modified theorem zorn.chain.total

modified def zorn.chain

modified theorem zorn.chain_chain_closure

modified theorem zorn.chain_closure_closure

modified theorem zorn.chain_closure_empty

modified theorem zorn.chain_closure_total

modified theorem zorn.chain_insert

modified theorem zorn.chain_succ

modified theorem zorn.exists_maximal_of_chains_bounded

modified def zorn.is_max_chain

modified theorem zorn.max_chain_spec

modified theorem zorn.succ_increasing

modified theorem zorn.succ_spec

added theorem zorn.zorn_superset

added theorem zorn.zorn_superset_nonempty