Commit 2025-02-18 13:54 ffb61743

View on Github →

chore(Order/Monotone): split Basic.lean into Basic.lean and Defs.lean (#22004) Order.Monotone.Basic is a rather large file and contains a mix of definitions and results. This PR splits it in two files:

Monotone.Defs contains the definition of Monotone, StrictMonotone, Antitone, etc, and proofs for basic functions such as identity, composition and product projections.
Monotone.Basic contains the remaining theory, especially that involving the order on natural numbers and integers.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean

Modified Mathlib/Algebra/Prime/Lemmas.lean

Modified Mathlib/Data/Nat/Choose/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

deleted theorem Antitone.comp_monotone

deleted theorem Antitone.comp_monotoneOn

deleted theorem Antitone.imp

deleted theorem Antitone.prod_map

deleted theorem Antitone.reflect_lt

deleted theorem Antitone.strictAnti_of_injective

deleted def Antitone

deleted theorem AntitoneOn.reflect_lt

deleted def AntitoneOn

deleted theorem Function.const_mono

deleted theorem Function.const_strictMono

deleted theorem Function.monotone_eval

deleted theorem Function.update_mono

deleted theorem Function.update_strictMono

deleted theorem Monotone.comp_antitone

deleted theorem Monotone.comp_antitoneOn

deleted theorem Monotone.comp_le_comp_left

deleted theorem Monotone.imp

deleted theorem Monotone.prod_map

deleted theorem Monotone.reflect_lt

deleted theorem Monotone.strictMono_of_injective

deleted def Monotone

deleted theorem MonotoneOn.reflect_lt

deleted def MonotoneOn

deleted theorem StrictAnti.comp_strictMono

deleted theorem StrictAnti.comp_strictMonoOn

deleted theorem StrictAnti.imp

deleted theorem StrictAnti.prod_map

deleted def StrictAnti

deleted def StrictAntiOn

deleted theorem StrictMono.comp_strictAnti

deleted theorem StrictMono.comp_strictAntiOn

deleted theorem StrictMono.imp

deleted theorem StrictMono.prod_map

deleted def StrictMono

deleted def StrictMonoOn

deleted theorem Subsingleton.antitone'

deleted theorem Subsingleton.monotone'

deleted theorem Subtype.mono_coe

deleted theorem Subtype.strictMono_coe

deleted theorem antitoneOn_const

deleted theorem antitoneOn_iff_forall_lt

deleted theorem antitoneOn_univ

deleted theorem antitone_app

deleted theorem antitone_const

deleted theorem antitone_iff_apply₂

deleted theorem antitone_iff_forall_lt

deleted theorem antitone_lam

deleted theorem antitone_prod_iff

deleted theorem injective_of_le_imp_le

deleted theorem injective_of_lt_imp_ne

deleted theorem monotoneOn_const

deleted theorem monotoneOn_id

deleted theorem monotoneOn_iff_forall_lt

deleted theorem monotoneOn_univ

deleted theorem monotone_app

deleted theorem monotone_const

deleted theorem monotone_fst

deleted theorem monotone_id

deleted theorem monotone_iff_apply₂

deleted theorem monotone_iff_forall_lt

deleted theorem monotone_lam

deleted theorem monotone_prod_iff

deleted theorem monotone_snd

deleted theorem strictAntiOn_univ

deleted theorem strictAnti_of_le_iff_le

deleted theorem strictMonoOn_id

deleted theorem strictMonoOn_univ

deleted theorem strictMono_id

deleted theorem strictMono_of_le_iff_le

Created Mathlib/Order/Monotone/Defs.lean

added theorem Antitone.comp_monotone

added theorem Antitone.comp_monotoneOn

added theorem Antitone.imp

added theorem Antitone.prod_map

added theorem Antitone.reflect_lt

added theorem Antitone.strictAnti_of_injective

added def Antitone

added theorem AntitoneOn.reflect_lt

added def AntitoneOn

added theorem Function.const_mono

added theorem Function.const_strictMono

added theorem Function.monotone_eval

added theorem Function.update_mono

added theorem Function.update_strictMono

added theorem Monotone.comp_antitone

added theorem Monotone.comp_antitoneOn

added theorem Monotone.comp_le_comp_left

added theorem Monotone.imp

added theorem Monotone.prod_map

added theorem Monotone.reflect_lt

added theorem Monotone.strictMono_of_injective

added def Monotone

added theorem MonotoneOn.reflect_lt

added def MonotoneOn

added theorem StrictAnti.comp_strictMono

added theorem StrictAnti.comp_strictMonoOn

added theorem StrictAnti.imp

added theorem StrictAnti.prod_map

added def StrictAnti

added def StrictAntiOn

added theorem StrictMono.comp_strictAnti

added theorem StrictMono.comp_strictAntiOn

added theorem StrictMono.imp

added theorem StrictMono.prod_map

added def StrictMono

added def StrictMonoOn

added theorem Subsingleton.antitone'

added theorem Subsingleton.monotone'

added theorem Subtype.mono_coe

added theorem Subtype.strictMono_coe

added theorem antitoneOn_const

added theorem antitoneOn_iff_forall_lt

added theorem antitoneOn_univ

added theorem antitone_app

added theorem antitone_const

added theorem antitone_iff_apply₂

added theorem antitone_iff_forall_lt

added theorem antitone_lam

added theorem antitone_prod_iff

added theorem injective_of_le_imp_le

added theorem injective_of_lt_imp_ne

added theorem monotoneOn_const

added theorem monotoneOn_id

added theorem monotoneOn_iff_forall_lt

added theorem monotoneOn_univ

added theorem monotone_app

added theorem monotone_const

added theorem monotone_fst

added theorem monotone_id

added theorem monotone_iff_apply₂

added theorem monotone_iff_forall_lt

added theorem monotone_lam

added theorem monotone_prod_iff

added theorem monotone_snd

added theorem strictAntiOn_univ

added theorem strictAnti_of_le_iff_le

added theorem strictMonoOn_id

added theorem strictMonoOn_univ

added theorem strictMono_id

added theorem strictMono_of_le_iff_le