Stream: math-comp analysis

Topic: entourage

view this post on Zulip Marie Kerjean (Sep 17 2020 at 06:31):

Now that the topological hierarchy includes entourage, what is the good way to prove that some set is a nbhsin a normed space ? Previously, applying locallyP let to an inductive goal allowing to apply exists r where r is the radius of a ball included in this nbhs. Now applying nbhsP leads to a goal mentioning entourage which I don't know how to handle.
At this point I have been using either nbhs_nbhs_norm or nbhs_ballP, and unfolding defintions as fmap to work around that.

view this post on Zulip Reynald Affeldt (Sep 17 2020 at 06:51):

Shouldn't applications of nbhsP be turned into applications fo nbhs_ballP to recover the same behavior? (At least that's why I read from the commit that introduced entourages.)

view this post on Zulip Marie Kerjean (Oct 12 2020 at 15:19):


Last updated: Jun 25 2024 at 19:01 UTC