Stream: math-comp analysis

Topic: balls are not provably open


view this post on Zulip 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 ?

view this post on Zulip Cyril Cohen (Dec 08 2020 at 21:09):

good point...

view this post on Zulip Cyril Cohen (Dec 08 2020 at 21:09):

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

view this post on Zulip Cyril Cohen (Dec 08 2020 at 21:11):

I am quite convince it does not....

view this post on Zulip 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]]a, b]

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (Dec 08 2020 at 22:26):

And I was proposing two solutions for that.


Last updated: Mar 28 2024 at 08:01 UTC