theorem Bornology.isBounded_vadd_set {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (s : Set (EuclideanSpace ℝ (Fin d))) (hs : IsBounded s) : IsBounded (a +ᵥ s)