no goals
𝓕 : Type ?u.98865
𝕜 : Type ?u.98868
α : Type ?u.98871
ι : Type ?u.98874
κ : Type ?u.98877
E : Type u_1
F : Type ?u.98883
G : Type ?u.98886
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ Bounded s ↔ ∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C
simpa only [Set.subset_def, mem_closedBall_one_iff] using bounded_iff_subset_ball (1 : E)