Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 13:01 c7745b3b

View on Github →

chore(order/zorn): Review (#12175) Lemma renames

Estimated changes

Modified src/analysis/convex/basic.lean

Modified src/analysis/convex/cone.lean

Modified src/analysis/inner_product_space/basic.lean

Modified src/data/set/pairwise.lean

added theorem set.pairwise.insert

added theorem set.pairwise.insert_of_symmetric

Modified src/field_theory/adjoin.lean

modified theorem intermediate_field.lifts.exists_max_three

modified theorem intermediate_field.lifts.exists_max_two

modified theorem intermediate_field.lifts.exists_upper_bound

modified def intermediate_field.lifts.upper_bound_intermediate_field

Modified src/field_theory/is_alg_closed/basic.lean

Modified src/group_theory/sylow.lean

Modified src/linear_algebra/linear_independent.lean

Modified src/measure_theory/covering/vitali.lean

Modified src/order/compactly_generated.lean

Modified src/order/extension.lean

Modified src/order/filter/ultrafilter.lean

Modified src/order/zorn.lean

added theorem chain_closure.is_chain

added theorem chain_closure.succ_fixpoint

added theorem chain_closure.succ_fixpoint_iff

added inductive chain_closure

added theorem chain_closure_empty

added theorem chain_closure_max_chain

added theorem chain_closure_total

deleted theorem directed_of_chain

added theorem exists_maximal_of_chains_bounded

added theorem exists_maximal_of_nonempty_chains_bounded

added theorem is_chain.directed

added theorem is_chain.directed_on

added theorem is_chain.exists_max_chain

added theorem is_chain.image

added theorem is_chain.insert

added theorem is_chain.mono

added theorem is_chain.succ

added theorem is_chain.super_chain_succ_chain

added theorem is_chain.symm

added theorem is_chain.total

added def is_chain

added theorem is_chain_empty

added theorem is_chain_of_trichotomous

added theorem is_chain_univ_iff

added theorem is_max_chain.is_chain

added theorem is_max_chain.not_super_chain

added def is_max_chain

added def max_chain

added theorem max_chain_spec

deleted theorem set.subsingleton.chain

added theorem set.subsingleton.is_chain

added def succ_chain

added theorem succ_increasing

added theorem succ_spec

added def super_chain

deleted theorem zorn.chain.directed_on

deleted theorem zorn.chain.image

deleted theorem zorn.chain.max_chain_of_chain

deleted theorem zorn.chain.mono

deleted theorem zorn.chain.symm

deleted theorem zorn.chain.total

deleted theorem zorn.chain.total_of_refl

deleted def zorn.chain

deleted theorem zorn.chain_chain_closure

deleted inductive zorn.chain_closure

deleted theorem zorn.chain_closure_closure

deleted theorem zorn.chain_closure_empty

deleted theorem zorn.chain_closure_succ_fixpoint

deleted theorem zorn.chain_closure_succ_fixpoint_iff

deleted theorem zorn.chain_closure_total

deleted theorem zorn.chain_empty

deleted theorem zorn.chain_insert

deleted theorem zorn.chain_of_trichotomous

deleted theorem zorn.chain_succ

deleted theorem zorn.chain_univ_iff

deleted theorem zorn.exists_maximal_of_chains_bounded

deleted theorem zorn.exists_maximal_of_nonempty_chains_bounded

deleted def zorn.is_max_chain

deleted def zorn.max_chain

deleted theorem zorn.max_chain_spec

deleted def zorn.succ_chain

deleted theorem zorn.succ_increasing

deleted theorem zorn.succ_spec

deleted def zorn.super_chain

deleted theorem zorn.super_of_not_max

deleted theorem zorn.zorn_nonempty_partial_order

deleted theorem zorn.zorn_nonempty_partial_order₀

deleted theorem zorn.zorn_partial_order

deleted theorem zorn.zorn_partial_order₀

deleted theorem zorn.zorn_subset

deleted theorem zorn.zorn_subset_nonempty

deleted theorem zorn.zorn_superset

deleted theorem zorn.zorn_superset_nonempty

added theorem zorn_nonempty_partial_order

added theorem zorn_nonempty_partial_order₀

added theorem zorn_partial_order

added theorem zorn_partial_order₀

added theorem zorn_subset

added theorem zorn_subset_nonempty

added theorem zorn_superset

added theorem zorn_superset_nonempty

Modified src/ring_theory/algebraic_independent.lean

Modified src/ring_theory/ideal/operations.lean

Modified src/set_theory/schroeder_bernstein.lean

Modified src/topology/algebra/semigroup.lean

Modified src/topology/shrinking_lemma.lean

modified theorem shrinking_lemma.partial_refinement.apply_eq_of_chain

modified def shrinking_lemma.partial_refinement.chain_Sup

modified theorem shrinking_lemma.partial_refinement.find_apply_of_mem

modified theorem shrinking_lemma.partial_refinement.le_chain_Sup

Modified src/topology/subset_properties.lean