Commit 2025-12-30 23:52 99a5a6fe

feat(Order/Monotone/Defs): weaken hypothesis of injective_of_le_imp_le (#33111) injective_of_le_imp_le requires ∀ x y, f x ≤ f y → x ≤ y, but ∀ x y, f x = f y → x ≤ y is sufficient. Also rename the weakenedinjective_of_le_imp_le to Function.Injective.of_eq_imp_le and injective_of_lt_imp_ne to Function.Injective.of_lt_imp_ne to allow for dot notation.