Commit 2024-11-14 00:39 14269a79

View on Github →

chore(Order/InitialSeg): rename various defs (#17989) This PR renames:

PrincipalSeg.ltLe → PrincipalSeg.transInitial
InitialSeg.leLT → InitialSeg.transPrincipal
PrincipalSeg.equivLT → PrincipalSeg.relIsoTrans
PrincipalSeg.ltEquiv → PrincipalSeg.transRelIso
InitialSeg.ltOrEq → InitialSeg.principalSumRelIso See Zulip.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.eq_principalSeg

added theorem InitialSeg.eq_relIso

deleted theorem InitialSeg.ltOrEq_apply_left

deleted theorem InitialSeg.ltOrEq_apply_right

added theorem InitialSeg.transPrincipal_apply

deleted def PrincipalSeg.equivLT

deleted def PrincipalSeg.ltEquiv

deleted def PrincipalSeg.ltLe

added def PrincipalSeg.relIsoTrans

added theorem PrincipalSeg.relIsoTrans_apply

added theorem PrincipalSeg.relIsoTrans_top

added def PrincipalSeg.transInitial

added theorem PrincipalSeg.transInitial_apply

added theorem PrincipalSeg.transInitial_top

added def PrincipalSeg.transRelIso

added theorem PrincipalSeg.transRelIso_apply

added theorem PrincipalSeg.transRelIso_top

modified theorem PrincipalSeg.trans_apply

Modified Mathlib/SetTheory/Ordinal/Basic.lean