Commit 2022-09-30 18:50 726746f4

View on Github →

feat: port order/monotone, needed for apply_fun (#441)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Monotone.lean

added theorem Antitone.imp

added theorem Antitone.strict_anti_of_injective

added def Antitone

added def AntitoneOn

added theorem Function.monotone_eval

added theorem Monotone.comp_le_comp_left

added theorem Monotone.imp

added theorem Monotone.strict_mono_of_injective

added def Monotone

added def MonotoneOn

added theorem StrictAnti.imp

added def StrictAnti

added def StrictAntiOn

added theorem StrictMono.imp

added def StrictMono

added def StrictMonoOn

added theorem Subsingleton.antitone'

added theorem Subsingleton.monotone'

added theorem antitone_app

added theorem antitone_const

added theorem antitone_iff_forall_lt

added theorem antitone_lam

added theorem antitone_on_const

added theorem antitone_on_iff_forall_lt

added theorem injective_of_le_imp_le

added theorem monotone_app

added theorem monotone_const

added theorem monotone_id

added theorem monotone_iff_forall_lt

added theorem monotone_lam

added theorem monotone_on_const

added theorem monotone_on_id

added theorem monotone_on_iff_forall_lt

added theorem strict_mono_id

added theorem strict_mono_on_id