M : Type u_1
N : Type ?u.167794
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ Set.Nonempty ↑S
M : Type u_1
N : Type ?u.167794
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(mk' S) m‖ = 0 ↔ m ∈ closure ↑S
rw [mk'_apply, norm_mk, ← mem_closure_iff_infDist_zero]
no goals
M : Type u_1
N : Type ?u.167794
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ Set.Nonempty ↑S
exact ⟨0, S.zero_mem⟩