Why does `open_nbhs_ball`

states that the interior of a ball is an open neighbourhood, and not the ball itself ?

```
open_nbhs_ball
: forall (x0 : ?M) (eps : {posnum ?R}), open_nbhs x0 (ball x0 (eps)%:num)^°
```

Am I missing the lemma saying that in a reasonable case, `ball`

is always open ?

good point...

maybe the interface of pseudoMetricType does not impose that...

I am quite convince it does not....

So in all generality, they can be open or close or anything in between... e.g. intervals $]a, b]$

either you also define `open_ball`

as the interior of a ball, or we refine the interface to reflect our prejudice about balls :laughing:

Maybe one doesn't need `open_ball`

, and at this point I should go back in Banach Steinhauss to try and remember what was the purpose of closed balls at all.

But implementing those lemmas needs to prove explicitely that `ball x r`

is open in our case, and I wonder if it still necessary.

We do not need or have to, however I believe it would be nice that balls are either open or close and to have the other...

And I was proposing two solutions for that.

Last updated: Feb 09 2023 at 03:06 UTC