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

deleted theorem antitone.comp_monotone
deleted theorem antitone.comp_monotone_on
deleted theorem antitone.reflect_lt
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 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.reflect_lt
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.injective
deleted theorem strict_anti.le_iff_le
deleted theorem strict_anti.lt_iff_lt
deleted def strict_anti
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.id_le
deleted theorem strict_mono.injective
deleted theorem strict_mono.le_iff_le
deleted theorem strict_mono.lt_iff_lt
deleted def strict_mono
deleted theorem strict_mono_id
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
added theorem antitone.comp_monotone
added theorem antitone.reflect_lt
added def antitone
added theorem antitone_app
added theorem antitone_const
added theorem antitone_lam
added def antitone_on
added theorem antitone_on_univ
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.reflect_lt
added def monotone
added theorem monotone_app
added theorem monotone_const
added theorem monotone_fst
added theorem monotone_id
added theorem monotone_lam
added def monotone_on
added theorem monotone_on_univ
added theorem monotone_snd
added theorem strict_anti.injective
added theorem strict_anti.le_iff_le
added theorem strict_anti.lt_iff_lt
added def strict_anti
added def strict_anti_on
added theorem strict_anti_on_univ
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 def strict_mono
added theorem strict_mono_id
added def strict_mono_on
added theorem strict_mono_on_univ
added theorem subtype.mono_coe