Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-03 20:33 465508fc

View on Github →

split(order/monotone): split off order.basic (#9518)

Estimated changes

Modified src/algebra/order/monoid_lemmas.lean

Modified src/order/basic.lean

deleted theorem antitone.comp_monotone

deleted theorem antitone.comp_monotone_on

deleted theorem antitone.ne_of_lt_of_lt_int

deleted theorem antitone.ne_of_lt_of_lt_nat

deleted theorem antitone.reflect_lt

deleted theorem antitone.strict_anti_iff_injective

deleted theorem antitone.strict_anti_of_injective

deleted def antitone

deleted theorem antitone_app

deleted theorem antitone_const

deleted theorem antitone_lam

deleted theorem antitone_nat_of_succ_le

deleted def antitone_on

deleted theorem antitone_on_univ

deleted theorem forall_ge_le_of_forall_le_succ

deleted theorem function.monotone_eval

deleted theorem injective_of_le_imp_le

deleted theorem injective_of_lt_imp_ne

deleted theorem monotone.comp_antitone

deleted theorem monotone.comp_antitone_on

deleted theorem monotone.comp_le_comp_left

deleted theorem monotone.ne_of_lt_of_lt_int

deleted theorem monotone.ne_of_lt_of_lt_nat

deleted theorem monotone.reflect_lt

deleted theorem monotone.strict_mono_iff_injective

deleted theorem monotone.strict_mono_of_injective

deleted def monotone

deleted theorem monotone_app

deleted theorem monotone_const

deleted theorem monotone_fst

deleted theorem monotone_id

deleted theorem monotone_lam

deleted theorem monotone_nat_of_le_succ

deleted def monotone_on

deleted theorem monotone_on_univ

deleted theorem monotone_snd

deleted theorem strict_anti.comp_strict_mono

deleted theorem strict_anti.comp_strict_mono_on

deleted theorem strict_anti.injective

deleted theorem strict_anti.le_iff_le

deleted theorem strict_anti.lt_iff_lt

deleted theorem strict_anti.maximal_of_minimal_image

deleted theorem strict_anti.minimal_of_maximal_image

deleted def strict_anti

deleted theorem strict_anti_nat_of_succ_lt

deleted theorem strict_anti_on.le_iff_le

deleted theorem strict_anti_on.lt_iff_lt

deleted def strict_anti_on

deleted theorem strict_anti_on_univ

deleted theorem strict_mono.comp_strict_anti

deleted theorem strict_mono.comp_strict_anti_on

deleted theorem strict_mono.id_le

deleted theorem strict_mono.injective

deleted theorem strict_mono.le_iff_le

deleted theorem strict_mono.lt_iff_lt

deleted theorem strict_mono.maximal_of_maximal_image

deleted theorem strict_mono.minimal_of_minimal_image

deleted def strict_mono

deleted theorem strict_mono_id

deleted theorem strict_mono_nat_of_lt_succ

deleted theorem strict_mono_of_le_iff_le

deleted theorem strict_mono_on.le_iff_le

deleted theorem strict_mono_on.lt_iff_lt

deleted def strict_mono_on

deleted theorem strict_mono_on_univ

deleted theorem subtype.mono_coe

deleted theorem subtype.strict_mono_coe

Modified src/order/closure.lean

Modified src/order/iterate.lean

Modified src/order/lattice.lean

Created src/order/monotone.lean

added theorem antitone.comp_monotone

added theorem antitone.comp_monotone_on

added theorem antitone.ne_of_lt_of_lt_int

added theorem antitone.ne_of_lt_of_lt_nat

added theorem antitone.reflect_lt

added theorem antitone.strict_anti_iff_injective

added theorem antitone.strict_anti_of_injective

added def antitone

added theorem antitone_app

added theorem antitone_const

added theorem antitone_lam

added theorem antitone_nat_of_succ_le

added def antitone_on

added theorem antitone_on_univ

added theorem forall_ge_le_of_forall_le_succ

added theorem function.monotone_eval

added theorem injective_of_le_imp_le

added theorem injective_of_lt_imp_ne

added theorem monotone.comp_antitone

added theorem monotone.comp_antitone_on

added theorem monotone.comp_le_comp_left

added theorem monotone.ne_of_lt_of_lt_int

added theorem monotone.ne_of_lt_of_lt_nat

added theorem monotone.reflect_lt

added theorem monotone.strict_mono_iff_injective

added theorem monotone.strict_mono_of_injective

added def monotone

added theorem monotone_app

added theorem monotone_const

added theorem monotone_fst

added theorem monotone_id

added theorem monotone_lam

added theorem monotone_nat_of_le_succ

added def monotone_on

added theorem monotone_on_univ

added theorem monotone_snd

added theorem strict_anti.comp_strict_mono

added theorem strict_anti.comp_strict_mono_on

added theorem strict_anti.injective

added theorem strict_anti.le_iff_le

added theorem strict_anti.lt_iff_lt

added theorem strict_anti.maximal_of_minimal_image

added theorem strict_anti.minimal_of_maximal_image

added def strict_anti

added theorem strict_anti_nat_of_succ_lt

added theorem strict_anti_on.le_iff_le

added theorem strict_anti_on.lt_iff_lt

added def strict_anti_on

added theorem strict_anti_on_univ

added theorem strict_mono.comp_strict_anti

added theorem strict_mono.comp_strict_anti_on

added theorem strict_mono.id_le

added theorem strict_mono.injective

added theorem strict_mono.le_iff_le

added theorem strict_mono.lt_iff_lt

added theorem strict_mono.maximal_of_maximal_image

added theorem strict_mono.minimal_of_minimal_image

added def strict_mono

added theorem strict_mono_id

added theorem strict_mono_nat_of_lt_succ

added theorem strict_mono_of_le_iff_le

added theorem strict_mono_on.le_iff_le

added theorem strict_mono_on.lt_iff_lt

added def strict_mono_on

added theorem strict_mono_on_univ

added theorem subtype.mono_coe

added theorem subtype.strict_mono_coe

Modified src/order/prime_ideal.lean