Theorem Function.Injective.of_lt_imp_ne

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_lt_imp_neView on Github →