Zulip Chat Archive

Stream: maths

Topic: times_cont_diff name


Patrick Massot (Feb 22 2022 at 17:35):

I know this has already been discussed, but I can't find the messages. I think we really need a shorter name for times_cont_diff. Using notations is not enough, this appears in a lot of lemma names. I've just spent two hours proving differentiability lemmas in the sphere eversion project and I have many more to prove. This is simply too long. I don't want something completely obscure like tcd but maybe we could at least remove the times_? @Sebastien Gouezel @Yury G. Kudryashov

Yury G. Kudryashov (Feb 22 2022 at 17:37):

What about smooth? I know that it is currently used in manifolds. I don't mind writing msmooth ∞ instead of smooth there.

Patrick Massot (Feb 22 2022 at 17:40):

smooth would sound weird for finite n

Floris van Doorn (Feb 22 2022 at 17:44):

maybe is_C, so is_C 𝕜 n f corresponds to fCnf \in C^n.
Probably to cryptic though.

Heather Macbeth (Feb 22 2022 at 17:48):

I think cont_diff sounds reasonable, indeed.

Sebastien Gouezel (Feb 22 2022 at 19:52):

Yes, cont_diff looks ok.

Yaël Dillies (Feb 22 2022 at 19:55):

I personally could never make the meaning times in this name. Is it "continuous differentiable that many times"? I thought it could also refer to`× somehow.

Patrick Massot (Feb 22 2022 at 20:44):

@Yury G. Kudryashov are you also ok with cont_diff?

Patrick Massot (Feb 22 2022 at 20:45):

If yes then I'll try to open a PR so that someone can merge it really fast. It should be as easy as a global search and replace.

Patrick Massot (Feb 22 2022 at 20:47):

VScode says times_cont_diff appears 1987 times in 31 files.

Patrick Massot (Feb 22 2022 at 20:49):

And add 799 hits for times_cont_mdiff

Damiano Testa (Feb 22 2022 at 20:53):

Surely nothing can go wrong when changing 2786 names in 31 files...

Patrick Massot (Feb 22 2022 at 20:55):

I opened #12227 without waiting for Yury's answer since creating the PR was very little work.

Yury G. Kudryashov (Feb 22 2022 at 21:09):

Thank you! I was away from computer for some time.


Last updated: Dec 20 2023 at 11:08 UTC