theorem Bornology.IsBddFun.const_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → E} {c : 𝕜} (hf : IsBddFun f) : IsBddFun (c • f)

theorem Bornology.IsBddFun.fun_const_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → E} {c : 𝕜} (hf : IsBddFun f) : IsBddFun fun (i : α) => c • f i

Eta-expanded form of Bornology.IsBddFun.const_smul