Stream: math-comp analysis

Topic: balls are not provably open

Marie Kerjean (Dec 08 2020 at 20:45):

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 ?

Cyril Cohen (Dec 08 2020 at 21:09):

good point...

Cyril Cohen (Dec 08 2020 at 21:09):

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

Cyril Cohen (Dec 08 2020 at 21:11):

I am quite convince it does not....

Cyril Cohen (Dec 08 2020 at 21:12):

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

Cyril Cohen (Dec 08 2020 at 21:13):

either you also define open_ball as the interior of a ball, or we refine the interface to reflect our prejudice about balls :laughing:

Marie Kerjean (Dec 08 2020 at 22:06):

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.

Marie Kerjean (Dec 08 2020 at 22:08):

But implementing those lemmas needs to prove explicitely that ball x r is open in our case, and I wonder if it still necessary.

Cyril Cohen (Dec 08 2020 at 22:26):

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...

Cyril Cohen (Dec 08 2020 at 22:26):

And I was proposing two solutions for that.

Last updated: Oct 13 2024 at 01:02 UTC