Commit 2024-11-11 17:29 d2a10de7

View on Github →

chore(Order/InitialSeg): InitialSeg.ofIso → RelIso.toInitialSeg (#18069) This enables dot notation.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

deleted def InitialSeg.ofIso

added def OrderIso.toInitialSeg

added def RelIso.toInitialSeg

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean