theorem Bornology.IsBddFun.mul {α : Type u_1} {E : Type u_2} [SeminormedGroup E] {f g : α → E} (hf : IsBddFun f) (hg : IsBddFun g) : IsBddFun (f * g)

theorem Bornology.IsBddFun.add {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {f g : α → E} (hf : IsBddFun f) (hg : IsBddFun g) : IsBddFun (f + g)