eball vs emetricBall vs EMetric.ball

Stream: mathlib4

[Yury G. Kudryashov]

How should we name lemmas about docs#EMetric.ball and docs#EMetric.closedBall ? Some lemmas use eball, others use emetricBall or put lemmas in the EMetric namespace (sometimes, it's not an option).

[Yaël Dillies]

I personally think we could drop the EMetric namespace entirely, renaming each EMetric.foo to Metric.efoo

[Yury G. Kudryashov]

eclosedBall or closedEBall?

[Yaël Dillies]

I don't mind greatly, but maybe the latter?

[Sébastien Gouëzel]

I'd go for eball and closedEBall.

[Snir Broshi]

I vote for eclosedBall

[Eric Wieser]

Another datapoint is docs#EMetric.infEdist

[Yury G. Kudryashov]

... which should be called infEDist.

[Eric Wieser]

Perhaps

[Yury G. Kudryashov]

At least, that's what we do with EDist and ENNReal.

[Yury G. Kudryashov]

Let's start with #33558

[Eric Wieser]

Repeating what I wrote there; can you propose the full set of proposed new def names to be approved here first?

[Eric Wieser]

I agree that it's easier to actually rename them in separate PRs, but I think we should make and approve the decision globally first

[Yury G. Kudryashov]

• EMetric.diam -> Metric.ediam
• EMetric.ball -> Metric.eball
• EMetric.closedBall -> Metric.closedEBall
• EMetric.infEdist -> Metric.infEDist
• EMetric.mem_nhds_iff etc -> Metric.mem_nhds_iff_eball or _iff_edist
• same for Metric.mem_nhds_iff etc

[Yury G. Kudryashov]

What did I miss?

[Eric Wieser]

(docs#Metric.mem_nhds_iff for reference)

[Yury G. Kudryashov]

Should we go forward with renaming or wait a bit more? In the latter case, what's a good time to wait before merging the first PR?

[Ruben Van de Velde]

Maybe a few more days

[Ruben Van de Velde]

Flagging @maintainers if anyone wants to comment

[Jireh Loreaux]

I'm in favor.

[Yury G. Kudryashov]

@Ruben Van de Velde How many days is "a few"? I don't want to go against someone's objections, but I don't want the PR to rot.

[Jireh Loreaux]

@Yury G. Kudryashov, if no one objects before tomorrow morning, I'll merge it.

[Yury G. Kudryashov]

I've merged master and fixed build.

[Jireh Loreaux]

@Yury G. Kudryashov

[Yury G. Kudryashov]

Next: #33772

[Yury G. Kudryashov]

I wrote a script to print all non-autodecl names with deprecation info, then compared the output on master and on that branch to

• make sure that all previously deprecated names are still there with the same date & newName;
• every old name except for a few instance names didn't go away; instead, it's deprecated with date 2026-01-08.

[Yury G. Kudryashov]

I'm a bit afraid that #33772 will rot.

[Matteo Cipollina]

during the review of #34202 @Michael Rothgang raised the question of whether should EMetric.annulus/i proposed in the PR be called Metric.eannulus instead, by analogy with Metric.eball and friends. I suspect the consensus is for a 'yes' but please let me know if any suggestion

[Yury G. Kudryashov]

I think, yes.

[Yury G. Kudryashov]

Next in line: #34379

[Yury G. Kudryashov]

I've left lemmas like docs#EMetric.isOpen_iff for another PR to make it a bit easier to review this one.

[Yury G. Kudryashov]

I've tested that

• all newly deprecated names use date 2026-01-24;
• all newly deprecated names exist as non-deprecated names on master;
• no name disappeared, all of them were deprecated instead.

[Yury G. Kudryashov]

One deprecation change the "target": Emetric.exists_smooth_forall_closedBall_subset.

[Yury G. Kudryashov]

#34379 regularly gets merge conflicts. I would appreciate a review.