Documentation
LeanPool
.
SardMoreira
.
Topology
Search
return to top
source
Imports
Init
Mathlib.Topology.NhdsWithin
Imported by
eventually_nhdsWithin_nhds
LeanPool.SardMoreira.Topology
#
source
theorem
eventually_nhdsWithin_nhds
{
X
:
Type
u_1}
[
TopologicalSpace
X
]
{
U
:
Set
X
}
(
hU
:
IsOpen
U
)
{
p
:
X
→
Prop
}
{
x
:
X
}
:
(
∀ᶠ
(
y
:
X
)
in
nhdsWithin
x
U
,
∀ᶠ
(
z
:
X
)
in
nhds
y
,
p
z
)
↔
∀ᶠ
(
y
:
X
)
in
nhdsWithin
x
U
,
p
y