Neighborhoods of a set #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define the filter
𝓝ˢ s or
nhds_set s consisting of all neighborhoods of a set
Main Properties #
There are a couple different notions equivalent to
s ∈ 𝓝ˢ t:
Furthermore, we have the following results:
The filter of neighborhoods of a set in a topological space.
Preimage of a set neighborhood of
t under a continuous map
f is a set neighborhood of