leLT, ltLe, and other naming weirdness

Stream: mathlib4

[Violeta Hernández]

Consider the following:

• docs#PrincipalSeg.ltLe
• docs#InitialSeg.leLT
• docs#PrincipalSeg.equivLT
• docs#PrincipalSeg.ltEquiv
• docs#InitialSeg.ltOrEq

[Violeta Hernández]

The naming scheme on display is all over the place, regarding capitalization of le/lt and usage of equiv/eq

[Violeta Hernández]

These definitions aren't even about order relations, mind you, but about compositions of, docs#InitialSeg (le), docs#PrincipalSeg (lt), and docs#RelIso (eq)

[Violeta Hernández]

I get what's being done here, but I feel like this just doesn't jive with our usual naming conventions. I'm not really sure how to rename these, though.

[Eric Wieser]

The first two look like they should be compInitial and similar

[Violeta Hernández]

Maybe transInitial instead? I think we generally use trans and such for embeddings like these

[Eric Wieser]

Sure, though watch out for the order reversal between comp and trans!

[Violeta Hernández]

So here's my suggestion

• docs#PrincipalSeg.ltLe → PrincipalSeg.transInitial
• docs#InitialSeg.leLT → InitialSeg.transPrincipal
• docs#PrincipalSeg.equivLT → PrincipalSeg.relIsoTrans
• docs#PrincipalSeg.ltEquiv → PrincipalSeg.transRelIso
• docs#InitialSeg.ltOrEq → InitialSeg.principalSumRelIso

[Violeta Hernández]

#17989