Exterior of a set

We define exterior s to be the intersection of all neighborhoods of s, see Mathlib/Topology/Defs/Filter.lean. Note that this construction has no standard name in the literature.

In this file we prove basic properties of this operation.

theorem exterior_singleton_eq_ker_nhds {X : Type u_2} [TopologicalSpace X] (x : X) : exterior {x} = (nhds x).ker

@[simp]

theorem mem_exterior_singleton {X : Type u_2} [TopologicalSpace X] {x y : X} : x ∈ exterior {y} ↔ x ⤳ y

theorem exterior_def {X : Type u_2} [TopologicalSpace X] (s : Set X) : exterior s = ⋂₀ {t : Set X | IsOpen t ∧ s ⊆ t}

theorem mem_exterior {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} : x ∈ exterior s ↔ ∀ (U : Set X), IsOpen U → s ⊆ U → x ∈ U

theorem subset_exterior_iff {X : Type u_2} [TopologicalSpace X] {s t : Set X} : s ⊆ exterior t ↔ ∀ (U : Set X), IsOpen U → t ⊆ U → s ⊆ U

theorem subset_exterior {X : Type u_2} [TopologicalSpace X] {s : Set X} : s ⊆ exterior s

theorem exterior_minimal {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t

theorem IsOpen.exterior_eq {X : Type u_2} [TopologicalSpace X] {s : Set X} (h : IsOpen s) : exterior s = s

theorem IsOpen.exterior_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t

@[simp]

theorem exterior_iUnion {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] (s : ι → Set X) : exterior (⋃ (i : ι), s i) = ⋃ (i : ι), exterior (s i)

@[simp]

theorem exterior_union {X : Type u_2} [TopologicalSpace X] (s t : Set X) : exterior (s ∪ t) = exterior s ∪ exterior t

@[simp]

theorem exterior_sUnion {X : Type u_2} [TopologicalSpace X] (S : Set (Set X)) : exterior (⋃₀ S) = ⋃ s ∈ S, exterior s

theorem mem_exterior_iff_specializes {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} : x ∈ exterior s ↔ ∃ y ∈ s, x ⤳ y

theorem exterior_mono {X : Type u_2} [TopologicalSpace X] : Monotone exterior

theorem exterior_subset_exterior {X : Type u_2} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) : exterior s ⊆ exterior t

This name was used to be used for the Iff version, see exterior_subset_exterior_iff_nhdsSet.

@[simp]

theorem exterior_subset_exterior_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} : exterior s ⊆ exterior t ↔ nhdsSet s ≤ nhdsSet t

theorem exterior_eq_exterior_iff_nhdsSet {X : Type u_2} [TopologicalSpace X] {s t : Set X} : exterior s = exterior t ↔ nhdsSet s = nhdsSet t

theorem specializes_iff_exterior_subset {X : Type u_2} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ exterior {x} ⊆ exterior {y}

theorem exterior_iInter_subset {ι : Sort u_1} {X : Type u_2} [TopologicalSpace X] {s : ι → Set X} : exterior (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), exterior (s i)

theorem exterior_inter_subset {X : Type u_2} [TopologicalSpace X] {s t : Set X} : exterior (s ∩ t) ⊆ exterior s ∩ exterior t

theorem exterior_sInter_subset {X : Type u_2} [TopologicalSpace X] {s : Set (Set X)} : exterior (⋂₀ s) ⊆ ⋂ x ∈ s, exterior x

@[simp]

theorem exterior_empty {X : Type u_2} [TopologicalSpace X] : exterior ∅ = ∅

@[simp]

theorem exterior_univ {X : Type u_2} [TopologicalSpace X] : exterior Set.univ = Set.univ

@[simp]

theorem exterior_eq_empty {X : Type u_2} [TopologicalSpace X] {s : Set X} : exterior s = ∅ ↔ s = ∅

@[simp]

theorem nhdsSet_exterior {X : Type u_2} [TopologicalSpace X] (s : Set X) : nhdsSet (exterior s) = nhdsSet s

@[simp]

theorem exterior_exterior {X : Type u_2} [TopologicalSpace X] (s : Set X) : exterior (exterior s) = exterior s