frontier_closed_ball'

Stream: maths

[Yaël Dillies]

Does docs#frontier_closed_ball' really need nontrivial E? What fails when E = unit?

[Patrick Massot]

The closed ball is {0} whose frontier is {0} and the sphere is empty.

[Junyan Xu]

Isn't the frontier also empty? Both the interior and the closure are {0}.

[Moritz Doll]

I think it is the other way round: boundary is empty, but the sphere is $\{0\}$.

[Junyan Xu]

Yes the sphere is {0} only when r=0. So when E is trivial you must add the condition r \ne 0.

[Moritz Doll]

I think it is better to have nontrivial E, because nobody cares about trivial normed spaces.

[Yaël Dillies]

Moritz, we have both :grinning: docs#frontier_closed_ball