naming convention: indexed propositions

Stream: mathlib4

[Eric Wieser]

For the indexed supremum and union, we have iSup and iUnion.

What name do we want for indexed propositions? We currently have:

• docs#LinearMap.IsOrthoᵢ (doesn't match iSup, and doesn't linkify on Zulip)
• docs#ProbabilityTheory.iIndepFun, docs#ProbabilityTheory.iIndepSet (breaks the CamelCase rule for Prop)

[Eric Wieser]

docs#Finset.disjiUnion has a relatedly-mangled name, where the i for "indexed" is lower case and incorrectly reads as part of disj

[Yaël Dillies]

I argued before this one should be called iDisjUnion

[Eric Wieser]

What's the rationale for choosing that over disjIUnion?

[Yaël Dillies]

That one-letter modifiers should always come first

[Eric Wieser]

/poll What should orthogonality of a family of vectors be called

• LinearMap.IsOrthoᵢ
• LinearMap.IIsOrtho
• LinearMap.iIsOrtho

[Yaël Dillies]

Similarly, people agreed with me before that docs#Filter.limsSup should be Filter.sLimsup

[Eric Wieser]

(same question applies to the indexed IndepFun and IndepSet and CondIndep and ...)

[Antoine Chambert-Loir]

Can you explain the rationale for the capitalized initial in the poll ?

[Eric Wieser]

#naming says that all types (which includes Props) should be CamelCase

[Antoine Chambert-Loir]

What to do with the present inconsistencies regarding #naming, then? For example docs#ProbabilityTheory.iIndepSet

[Yaël Dillies]

(Antoine, have you read the start of the thread?)

[Antoine Chambert-Loir]

(Yes, this is why I ask.)

[Eric Wieser]

The poll above is assuming we change everything to be consistent, and asking which choice we want to have everywhere

[Eric Wieser]

Hence this message

[Antoine Chambert-Loir]

(I explain my vote: I see the first letter s, i, etc. as a modifier, somewhat distinct from the rest of the type. Also, double I is not legible, and I usually prefer to avoid Unicode characters.)

[Eric Wieser]

If we go for the i prefix, then the outcome will also be to change #naming I guess

[Antoine Chambert-Loir]

(unless you wish to perpetuate this kind of discussion, yes…)

[Eric Rodriguez]

I guess it's nice having it be lower-case at the start - it makes it super easy to search for indexed propositions (when autocomplete finally works...)