Def RelIso.toInitialSeg

Modification history

2024-11-11 17:29

Mathlib/Order/InitialSeg.lean

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

Added RelIso.toInitialSeg View on Github →