Description: The neighborhoods of a point P for the topology induced by an uniform space U . (Contributed by Thierry Arnoux, 11-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | utoptop.1 | |
|
utopsnneip.1 | |
||
utopsnneip.2 | |
||
Assertion | utopsnneiplem | |