Naming conventions: namespace only to enable dot notation?

Stream: mathlib4

[Martin Winter]

We are implementing faces for cones and predicates for polyhedral cones and wonder about mathlib naming conventions:

We implemented the predicate F.IsFaceOf C which states that the pointed cone F is a face of the pointed cone C. How should lemmas for this predicate be called? For example, if a lemma takes a hypothesis (h : F.IsFaceOf C) as input, I name it IsFaceOf.foo to make use of the dot notation. But if the lemma has no such hypothesis, do I still put it into the IsFaceOf namespace, or do I put it into the PointedCone namespace and call it isFaceOf_foo or so? An example of the latter would be the lemma that states that the lineality space of a cone is always a face. I have seen it done like this, e.g. for exists_isCompl is not in the IsCompl namespace.

Likewise for the predicate C.IsPolyhedral which states that C is a polyhedral cone. Consider the lemma that states that a finitely generated cone is polyhedral. Should it be

• IsPolyhedral.of_fg or
• PointedCone.isPolyhedral_of_fg or
• PointedCone.FG.isPolyhedral
• ...

Are there global rules or is it more important to be consistent within our small part of mathlib?

[Yaël Dillies]

The rules are simply to make use of as much dot notation as is reasonable. Here, both IsPolyhedral.of_fg and FG.isPolyhedral sound reasonable, so I would have them both