Commit 2024-01-14 18:19 6dd549bf

feat: action on UniformOnFun is uniformly continuous (#9714)

• add UniformInducing.uniformContinuousConstSMul and its additive version;
• use it to prove that the pointwise actions on α →ᵤ X and α →ᵤ[𝔖] X are uniformly continuous;
• use the latter facts to prove that the pointwise action on E →SL[σ] F is uniformly continuous;
• make M explicit in ContinuousLinearMap.strongTopology.continuousConstSMul, drop unneeded arguments.