metric bounded for normed space

Stream: Is there code for X?

[Adam Topaz]

I'm sure there is a lemma that gives the equivalence of docs#metric.bounded with being contained in a closed ball of a certain radius centered at zero for a normed space, but I can't seem to find it...

[Eric Rodriguez]

docs#metric.bounded_iff_subset_ball? or is this the wrong ball

[Adam Topaz]

Oh that should work.

[Adam Topaz]

thanks!