Exterior of a set #
We define exterior s
to be the intersection of all neighborhoods of s
,
see Topology/Defs/Filter
.
Note that this construction has no standard name in the literature.
In this file we prove basic properties of this operation.
@[simp]
theorem
exterior_minimal
{X : Type u_2}
[TopologicalSpace X]
{s : Set X}
{t : Set X}
(h₁ : s ⊆ t)
(h₂ : IsOpen t)
:
@[deprecated IsOpen.exterior_subset]
theorem
IsOpen.exterior_subset_iff
{X : Type u_2}
[TopologicalSpace X]
{s : Set X}
{t : Set X}
(ht : IsOpen t)
:
Alias of IsOpen.exterior_subset
.
@[simp]
@[simp]
theorem
exterior_subset_exterior
{X : Type u_2}
[TopologicalSpace X]
{s : Set X}
{t : Set X}
(h : s ⊆ t)
:
This name was used to be used for the Iff
version,
see exterior_subset_exterior_iff_nhdsSet
.
@[simp]
@[simp]
@[simp]