Commit 2025-05-14 14:51 b145a856

View on Github →

chore: move StrictMonoOn f s → InjOn f s earlier (#23424) This is motivated by the need to have these lemmas early in #23177.

Estimated changes

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/Data/Int/Lemmas.lean

Modified Mathlib/Data/Set/Monotone.lean

deleted theorem StrictAntiOn.comp

deleted theorem StrictAntiOn.comp_strictMonoOn

deleted theorem StrictAntiOn.injOn

deleted theorem StrictMonoOn.comp

deleted theorem StrictMonoOn.comp_strictAntiOn

deleted theorem StrictMonoOn.injOn

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/Hom/Set.lean

Modified Mathlib/Order/Interval/Set/Monotone.lean

Modified Mathlib/Order/ModularLattice.lean

Modified Mathlib/Order/Monotone/Basic.lean

added theorem StrictAntiOn.injOn

added theorem StrictMonoOn.injOn

Modified Mathlib/Order/Monotone/Defs.lean

added theorem StrictAntiOn.comp

added theorem StrictAntiOn.comp_strictMonoOn

added theorem StrictMonoOn.comp

added theorem StrictMonoOn.comp_strictAntiOn

Modified Mathlib/Order/Monotone/Extension.lean