unit_closedBall or unitClosedBall

Stream: mathlib4

[Eric Wieser]

Which of these is the correct name for lemmas about closedBall (0 : E) 1? We also have closed_unit_ball and closedUnitBall, but those ones seems obviously wrong to me.

[Eric Wieser]

/poll Which names should be used in lemmas?

• unit_ball, unit_closedBall, unit_sphere
• unitBall, unitClosedBall, unitSphere

[Eric Wieser]

Is the winning answer right now indicative that we should introduce abbrev unitBall := ball 0 1 etc?

[Oliver Nash]

No, because I just changed my mind ;-)

[Thomas Murrills]

Wait, why does closedUnitBall seem obviously wrong? I think I’d only ever say “closed unit ball”, never “unit closed ball”…

[Eric Wieser]

Because closedUnitBall does not contain closedBall as a substring, which is what the #naming guide mandates

[Eric Wieser]

closedUnitBall would be fine if we had abbrev closedUnitBall

[Eric Wieser]

(/ vs \, whoops)

[Eric Wieser]

/poll Should we introduce abbrevs for unit balls, so that we can pick more natural names?

• Yes
• No

[Thomas Murrills]

Ah, obviously wrong on naming convention grounds (at present), not on sounding-right grounds, got it :)

[Ruben Van de Velde]

Hmm, couldn't ball_one apply to any ball with radius one, not just those centered at zero?

[Kevin Buzzard]

Can we not also have "the unit ball with centre P"?

[Eric Wieser]

Pinging this thread, since the vote is a bit split

[Jireh Loreaux]

Why I voted for unitBall and friends: in other places, we sometimes modify the actual name of a declaration as it appears in names of other declartions. When we do this, I think we often include the modification as part of the lowerCamelCase bit, not separated with _. I'm thinking of things like docs#LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace where orthgonalComplement refers to Submodule.orthogonal.

[Yaël Dillies]

For people reading this thread, #9755 is now available for review