M : Type u_1
N : Type ?u.194075
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ (∃ x_1, x_1 ∈ {m | ↑(mk' S) m = x} ∧ ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
M : Type u_1
N : Type ?u.194075
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
rw [isGLB_lt_iff (isGLB_quotient_norm _), bex_image_iff]
no goals
M : Type u_1
N : Type ?u.194075
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ (∃ x_1, x_1 ∈ {m | ↑(mk' S) m = x} ∧ ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
rfl