Def OrderIso.toInitialSeg

Modification history

2024-11-11 17:29

Mathlib/Order/InitialSeg.lean

chore(Order/InitialSeg): `InitialSeg.ofIso` → `RelIso.toInitialSeg` (#18069) …

Added OrderIso.toInitialSeg View on Github →