Naming convention for infix-like defintions

Stream: mathlib4

[Dexin Zhang]

Currently theorems about Set.pi are named infix-like, that a theorem of Set.pi aaa bbb is named as aaa_pi_bbb (or aaa_pi, pi_bbb when one is a variable). E.g. docs#Set.univ_pi_empty, docs#Set.insert_pi, docs#Set.pi_univ, docs#Set.pi_update_of_mem.

There could be some argument; in #28665 @Christian Merten suggests we should follow the ordering in function application since there is no infix notation for Set.pi, while @Eric Wieser suggests we already allow infix-like style names even if there is no notation.

Do we have a naming convention for infix-like definitions? If not, can we reach an agreement?

For the case of Set.pi, I would be in favor of allowing such infix-like names; otherwise, it would be hard to decide how to name pi univ s and pi s univ.

[Notification Bot]

This topic was moved here from #mathlib4 > Naming convention for `Set.pi` by Dexin Zhang.

[Yaël Dillies]

Currently it's all up to feeling. I agree that it is somewhat weird that pi is being infixed when it enjoys no infix notation