Marie Kerjean (Sep 17 2020 at 06:31): 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.
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.)
Marie Kerjean (Oct 12 2020 at 15:19):(deleted)
Last updated: Apr 18 2024 at 22:02 UTC