Theorem Function.Injective.of_eq_imp_le

Modification history

2025-12-30 23:52
Mathlib/Order/Monotone/Defs.lean
feat(Order/Monotone/Defs): weaken hypothesis of `injective_of_le_imp_le` (#33111) …
Added Function.Injective.of_eq_imp_leView on Github →