Theorem OrderEmbedding.range_inj

Modification history

2024-09-17 10:56
Mathlib/Order/Hom/Set.lean
feat(Order/InitialSeg): Subsingleton (α ≃o β) on well-orders (#16882) …
Modified OrderEmbedding.range_injView on Github →
2024-09-17 07:27
Mathlib/Order/Hom/Set.lean
feat(Order/WellFounded): Generalize `StrictMono.id_le` (#16706) …
Added OrderEmbedding.range_injView on Github →