HasContinuousSMul naming

Stream: mathlib4

[Moritz Doll]

I've had a look at @Yury G. Kudryashov's PR and I am now confused about the naming convention again: we have has_smul -> SMul, but has_continuous_const_smul -> HasContinousConstSMul, which in my eyes should be ContinuousConstSMul and consequently in the MulAction PR we have ContinuousSMul, right?
cc @Ruben Van de Velde

[Yury G. Kudryashov]

I think, I forgot to change the name mathport gave me.

[Yury G. Kudryashov]

BTW, should we rename HasSup/HasInf to Sup/Inf?

[Moritz Doll]

My issue is that https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Topology/Algebra/ConstMulAction.lean is already wrong I think

[Yury G. Kudryashov]

I meant that I forgot to change the name in !4#2012

[Moritz Doll]

ah alright. @HasSup I would say yes (and I changed HasContinuousSup to ContinuousSup in !4#2129)

[Ruben Van de Velde]

Yeah, seems plausible that we should drop the Has there and in a bunch of other places

[Moritz Doll]

Ok, I will make a PR for HasContinuousConstSMul

[Moritz Doll]

!4#2185