Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-31 17:21 de503895

View on Github →

split(order/chain): Split off order.zorn (#13060) Split order.zorn into two files, one about chains, the other one about Zorn's lemma.

Estimated changes

added theorem chain_closure.is_chain
added theorem chain_closure.total
added inductive chain_closure
added theorem chain_closure_empty
added theorem is_chain.directed_on
added theorem is_chain.image
added theorem is_chain.insert
added theorem is_chain.mono
added theorem is_chain.succ
added theorem is_chain.symm
added theorem is_chain.total
added def is_chain
added theorem is_chain_empty
added theorem is_chain_univ_iff
added theorem is_max_chain.is_chain
added def is_max_chain
added def max_chain
added theorem max_chain_spec
added theorem subset_succ_chain
added def succ_chain
added theorem succ_chain_spec
added def super_chain
deleted theorem chain_closure.is_chain
deleted inductive chain_closure
deleted theorem chain_closure_empty
deleted theorem chain_closure_max_chain
deleted theorem chain_closure_total
deleted theorem is_chain.directed
deleted theorem is_chain.directed_on
deleted theorem is_chain.image
deleted theorem is_chain.insert
deleted theorem is_chain.mono
deleted theorem is_chain.succ
deleted theorem is_chain.symm
deleted theorem is_chain.total
deleted def is_chain
deleted theorem is_chain_empty
deleted theorem is_chain_of_trichotomous
deleted theorem is_chain_univ_iff
deleted theorem is_max_chain.is_chain
deleted def is_max_chain
deleted def max_chain
deleted theorem max_chain_spec
deleted theorem set.subsingleton.is_chain
deleted def succ_chain
deleted theorem succ_increasing
deleted theorem succ_spec
deleted def super_chain