Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-31 17:20 033a131a

View on Github →

chore(order/zorn): add module docstring (#7767) add module docstring, tidy up notation a bit

Estimated changes

Modified src/order/zorn.lean

modified theorem directed_of_chain

modified theorem zorn.chain.directed_on

modified theorem zorn.chain.image

modified theorem zorn.chain.mono

modified theorem zorn.chain.symm

modified theorem zorn.chain.total

modified theorem zorn.chain.total_of_refl

modified theorem zorn.chain_chain_closure

modified inductive zorn.chain_closure

modified theorem zorn.chain_closure_closure

modified theorem zorn.chain_closure_empty

modified theorem zorn.chain_closure_succ_fixpoint

modified theorem zorn.chain_closure_succ_fixpoint_iff

modified theorem zorn.chain_closure_total

modified theorem zorn.chain_insert

modified theorem zorn.chain_succ

modified theorem zorn.succ_increasing

modified theorem zorn.succ_spec

modified theorem zorn.super_of_not_max