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_ballP, and unfolding defintions as
fmap to work around that.
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.)
Last updated: Feb 05 2023 at 08:28 UTC