Commit 2022-11-18 09:07 8722e201

View on Github →

feat: port Order.Monotone (#591) mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

depends on: #567
depends on: #560
depends on: #569

Estimated changes

Modified Mathlib/Init/Set.lean

Modified Mathlib/Order/Monotone.lean

added theorem Antitone.comp_monotoneOn

added theorem Antitone.ne_of_lt_of_lt_int

added theorem Antitone.ne_of_lt_of_lt_nat

added theorem Antitone.prod_map

added theorem Antitone.reflect_lt

added theorem Antitone.strictAnti_iff_injective

added theorem Antitone.strictAnti_of_injective

deleted theorem Antitone.strict_anti_of_injective

added theorem AntitoneOn.reflect_lt

added theorem Function.const_mono

added theorem Function.const_strictMono

added theorem Int.exists_strictAnti

added theorem Int.exists_strictMono

added theorem Int.rel_of_forall_rel_succ_of_le

added theorem Int.rel_of_forall_rel_succ_of_lt

added theorem List.foldl_monotone

added theorem List.foldl_strictMono

added theorem List.foldr_monotone

added theorem List.foldr_strictMono

added theorem Monotone.comp_antitoneOn

added theorem Monotone.ne_of_lt_of_lt_int

added theorem Monotone.ne_of_lt_of_lt_nat

added theorem Monotone.prod_map

added theorem Monotone.reflect_lt

added theorem Monotone.strictMono_iff_injective

added theorem Monotone.strictMono_of_injective

deleted theorem Monotone.strict_mono_of_injective

added theorem MonotoneOn.reflect_lt

added theorem Nat.exists_strictAnti'

added theorem Nat.exists_strictAnti

added theorem Nat.exists_strictMono'

added theorem Nat.exists_strictMono

added theorem Nat.rel_of_forall_rel_succ_of_le

added theorem Nat.rel_of_forall_rel_succ_of_le_of_le

added theorem Nat.rel_of_forall_rel_succ_of_le_of_lt

added theorem Nat.rel_of_forall_rel_succ_of_lt

added theorem StrictAnti.cmp_map_eq

added theorem StrictAnti.comp_strictMono

added theorem StrictAnti.comp_strictMonoOn

added theorem StrictAnti.injective

added theorem StrictAnti.isMax_of_apply

added theorem StrictAnti.isMin_of_apply

added theorem StrictAnti.le_iff_le

added theorem StrictAnti.lt_iff_lt

added theorem StrictAnti.maximal_of_minimal_image

added theorem StrictAnti.minimal_of_maximal_image

added theorem StrictAnti.prod_map

added theorem StrictAntiOn.cmp_map_eq

added theorem StrictAntiOn.eq_iff_eq

added theorem StrictAntiOn.le_iff_le

added theorem StrictAntiOn.lt_iff_lt

added theorem StrictMono.cmp_map_eq

added theorem StrictMono.comp_strictAnti

added theorem StrictMono.comp_strictAntiOn

added theorem StrictMono.id_le

added theorem StrictMono.injective

added theorem StrictMono.isMax_of_apply

added theorem StrictMono.isMin_of_apply

added theorem StrictMono.le_iff_le

added theorem StrictMono.lt_iff_lt

added theorem StrictMono.maximal_of_maximal_image

added theorem StrictMono.minimal_of_minimal_image

added theorem StrictMono.prod_map

added theorem StrictMonoOn.cmp_map_eq

added theorem StrictMonoOn.eq_iff_eq

added theorem StrictMonoOn.le_iff_le

added theorem StrictMonoOn.lt_iff_lt

added theorem Subtype.mono_coe

added theorem Subtype.strictMono_coe

added theorem antitoneOn_comp_ofDual_iff

added theorem antitoneOn_const

added theorem antitoneOn_iff_forall_lt

added theorem antitoneOn_toDual_comp_iff

added theorem antitoneOn_univ

added theorem antitone_comp_ofDual_iff

added theorem antitone_int_of_succ_le

added theorem antitone_nat_of_succ_le

deleted theorem antitone_on_const

deleted theorem antitone_on_iff_forall_lt

added theorem antitone_toDual_comp_iff

modified theorem injective_of_le_imp_le

added theorem injective_of_lt_imp_ne

added theorem monotoneOn_comp_ofDual_iff

added theorem monotoneOn_const

added theorem monotoneOn_id

added theorem monotoneOn_iff_forall_lt

added theorem monotoneOn_toDual_comp_iff

added theorem monotoneOn_univ

added theorem monotone_comp_ofDual_iff

added theorem monotone_fst

added theorem monotone_int_of_le_succ

added theorem monotone_nat_of_le_succ

deleted theorem monotone_on_const

deleted theorem monotone_on_id

deleted theorem monotone_on_iff_forall_lt

added theorem monotone_snd

added theorem monotone_toDual_comp_iff

added theorem strictAntiOn_comp_ofDual_iff

added theorem strictAntiOn_toDual_comp_iff

added theorem strictAntiOn_univ

added theorem strictAnti_comp_ofDual_iff

added theorem strictAnti_int_of_succ_lt

added theorem strictAnti_nat_of_succ_lt

added theorem strictAnti_of_le_iff_le

added theorem strictAnti_toDual_comp_iff

added theorem strictMonoOn_comp_ofDual_iff

added theorem strictMonoOn_id

added theorem strictMonoOn_toDual_comp_iff

added theorem strictMonoOn_univ

added theorem strictMono_comp_ofDual_iff

added theorem strictMono_id

added theorem strictMono_int_of_lt_succ

added theorem strictMono_nat_of_lt_succ

added theorem strictMono_of_le_iff_le

added theorem strictMono_toDual_comp_iff

deleted theorem strict_mono_id

deleted theorem strict_mono_on_id