[Merged by Bors] - feat(Analysis/Normed/Group/Basic): add mem_closedBall_iff_nnnorm - #43752

[Merged by Bors] - feat(Analysis/Normed/Group/Basic): add mem_closedBall_iff_nnnorm#43752

b-mehta wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

b-mehta:feat/mem-closedBall-iff-nnnormb-mehta/mathlib4:feat/mem-closedBall-iff-nnnormCopy head branch name to clipboard