Theorem StrictMono.range_inj

Modification history

2024-09-17 07:27

Mathlib/Order/WellFounded.lean

feat(Order/WellFounded): Generalize `StrictMono.id_le` (#16706) …

Added StrictMono.range_inj View on Github →