E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ Bounded s → Bounded s⁻¹
simp_rw [bounded_iff_forall_norm_le', ← image_inv, ball_image_iff, norm_inv']
no goals
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C
exact id