Now that the topological hierarchy includes `entourage`

, what is the good way to prove that some set is a `nbhs`

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

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

(deleted)

Last updated: Feb 05 2023 at 08:28 UTC