# Interior, closure and frontier of a set #

This file provides lemmas relating to the functions `interior`, `closure` and `frontier` of a set endowed with a topology.

## Notation #

- `𝓝 x`: the filter `nhds x` of neighborhoods of a point `x`;
- `𝓟 s`: the principal filter of a set `s`;
- `𝓝[s] x`: the filter `nhdsWithin x s` of neighborhoods of a point `x` within a set `s`;
- `𝓝[≠] x`: the filter `nhdsWithin x {x}ᶜ` of punctured neighborhoods of `x`.

## Tags #

interior, closure, frontier

source
theorem mem_interior {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} :
x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
source
@[simp]
theorem isOpen_interior {X : Type u} [TopologicalSpace X] {s : Set X} :
IsOpen (interior s)
source
theorem interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s ⊆ s
source
theorem interior_maximal {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : t ⊆ s) (h₂ : IsOpen t) :
t ⊆ interior s
source
theorem IsOpen.interior_eq {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsOpen s) :
interior s = s
source
theorem interior_eq_iff_isOpen {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s = s ↔ IsOpen s
source
theorem subset_interior_iff_isOpen {X : Type u} [TopologicalSpace X] {s : Set X} :
s ⊆ interior s ↔ IsOpen s
source
theorem IsOpen.subset_interior_iff {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : IsOpen s) :
s ⊆ interior t ↔ s ⊆ t
source
theorem subset_interior_iff {X : Type u} [TopologicalSpace X] {s t : Set X} :
t ⊆ interior s ↔ ∃ (U : Set X), IsOpen U ∧ t ⊆ U ∧ U ⊆ s
source
theorem interior_subset_iff {X : Type u} [TopologicalSpace X] {s t : Set X} :
interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t
source
theorem interior_mono {X : Type u} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) :
interior s ⊆ interior t
source
theorem subset_interior_union {X : Type u} [TopologicalSpace X] {s t : Set X} :
interior s ∪ interior t ⊆ interior (s ∪ t)
source
@[simp]
theorem interior_empty {X : Type u} [TopologicalSpace X] :
interior ∅ = ∅
source
@[simp]
theorem interior_univ {X : Type u} [TopologicalSpace X] :
interior Set.univ = Set.univ
source
@[simp]
theorem interior_eq_univ {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s = Set.univ ↔ s = Set.univ
source
@[simp]
theorem interior_interior {X : Type u} [TopologicalSpace X] {s : Set X} :
interior (interior s) = interior s
source
@[simp]
theorem interior_inter {X : Type u} [TopologicalSpace X] {s t : Set X} :
interior (s ∩ t) = interior s ∩ interior t
source
theorem Set.Finite.interior_biInter {X : Type u} [TopologicalSpace X] {ι : Type u_1} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i)
source
theorem Set.Finite.interior_sInter {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : S.Finite) :
interior (⋂₀ S) = ⋂ s ∈ S, interior s
source
@[simp]
theorem Finset.interior_iInter {X : Type u} [TopologicalSpace X] {ι : Type u_1} (s : Finset ι) (f : ι → Set X) :
interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i)
source
@[simp]
theorem interior_iInter_of_finite {X : Type u} [TopologicalSpace X] {ι : Sort v} [Finite ι] (f : ι → Set X) :
interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
source
@[simp]
theorem interior_iInter₂_lt_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :
interior (⋂ (m : ℕ), ⋂ (_ : m < n), f m) = ⋂ (m : ℕ), ⋂ (_ : m < n), interior (f m)
source
@[simp]
theorem interior_iInter₂_le_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :
interior (⋂ (m : ℕ), ⋂ (_ : m ≤ n), f m) = ⋂ (m : ℕ), ⋂ (_ : m ≤ n), interior (f m)
source
theorem interior_union_inter_interior_compl_left_subset {X : Type u} [TopologicalSpace X] {s t : Set X} :
interior (s ∪ t) ∩ interior s ᶜ ⊆ interior t
source
theorem interior_union_inter_interior_compl_right_subset {X : Type u} [TopologicalSpace X] {s t : Set X} :
interior (s ∪ t) ∩ interior t ᶜ ⊆ interior s
source
theorem interior_union_isClosed_of_interior_empty {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : IsClosed s) (h₂ : interior t = ∅) :
interior (s ∪ t) = interior s
source
theorem isOpen_iff_forall_mem_open {X : Type u} [TopologicalSpace X] {s : Set X} :
IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
source
theorem interior_iInter_subset {X : Type u} [TopologicalSpace X] {ι : Sort v} (s : ι → Set X) :
interior (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), interior (s i)
source
theorem interior_iInter₂_subset {X : Type u} [TopologicalSpace X] {ι : Sort v} (p : ι → Sort u_1) (s : (i : ι) → p i → Set X) :
interior (⋂ (i : ι), ⋂ (j : p i), s i j) ⊆ ⋂ (i : ι), ⋂ (j : p i), interior (s i j)
source
theorem interior_sInter_subset {X : Type u} [TopologicalSpace X] (S : Set (Set X)) :
interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s
source
theorem Filter.HasBasis.lift'_interior {X : Type u} [TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) :
(l.lift' interior).HasBasis p fun (i : ι) => interior (s i)
source
theorem Filter.lift'_interior_le {X : Type u} [TopologicalSpace X] (l : Filter X) :
l.lift' interior ≤ l
source
theorem Filter.HasBasis.lift'_interior_eq_self {X : Type u} [TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) (ho : ∀ (i : ι), p i → IsOpen (s i)) :
l.lift' interior = l
source
@[simp]
theorem isClosed_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
IsClosed (closure s)
source
theorem subset_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
s ⊆ closure s
source
theorem notMem_of_notMem_closure {X : Type u} [TopologicalSpace X] {s : Set X} {P : X} (hP : P ∉ closure s) :
P ∉ s
source
@[deprecated notMem_of_notMem_closure (since := "2025-05-23")]
theorem not_mem_of_not_mem_closure {X : Type u} [TopologicalSpace X] {s : Set X} {P : X} (hP : P ∉ closure s) :
P ∉ s

Alias of `notMem_of_notMem_closure`.

source
theorem closure_minimal {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsClosed t) :
closure s ⊆ t
source
theorem Disjoint.closure_left {X : Type u} [TopologicalSpace X] {s t : Set X} (hd : Disjoint s t) (ht : IsOpen t) :
Disjoint (closure s) t
source
theorem Disjoint.closure_right {X : Type u} [TopologicalSpace X] {s t : Set X} (hd : Disjoint s t) (hs : IsOpen s) :
Disjoint s (closure t)
source
@[simp]
theorem IsClosed.closure_eq {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsClosed s) :
closure s = s
source
theorem IsClosed.closure_subset {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) :
closure s ⊆ s
source
theorem IsClosed.closure_subset_iff {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : IsClosed t) :
closure s ⊆ t ↔ s ⊆ t
source
theorem IsClosed.mem_iff_closure_subset {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsClosed s) :
x ∈ s ↔ closure {x} ⊆ s
source
theorem closure_mono {X : Type u} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) :
closure s ⊆ closure t
source
theorem monotone_closure (X : Type u_1) [TopologicalSpace X] :
Monotone closure
source
theorem closure_inter_subset {X : Type u} [TopologicalSpace X] {s t : Set X} :
closure (s ∩ t) ⊆ closure s ∩ closure t
source
theorem diff_subset_closure_iff {X : Type u} [TopologicalSpace X] {s t : Set X} :
s \ t ⊆ closure t ↔ s ⊆ closure t
source
theorem closure_inter_subset_inter_closure {X : Type u} [TopologicalSpace X] (s t : Set X) :
closure (s ∩ t) ⊆ closure s ∩ closure t
source
theorem isClosed_of_closure_subset {X : Type u} [TopologicalSpace X] {s : Set X} (h : closure s ⊆ s) :
IsClosed s
source
theorem closure_eq_iff_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} :
closure s = s ↔ IsClosed s
source
theorem closure_subset_iff_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} :
closure s ⊆ s ↔ IsClosed s
source
theorem closure_empty {X : Type u} [TopologicalSpace X] :
closure ∅ = ∅
source
@[simp]
theorem closure_empty_iff {X : Type u} [TopologicalSpace X] (s : Set X) :
closure s = ∅ ↔ s = ∅
source
@[simp]
theorem closure_nonempty_iff {X : Type u} [TopologicalSpace X] {s : Set X} :
(closure s).Nonempty ↔ s.Nonempty
source
theorem Set.Nonempty.closure {X : Type u} [TopologicalSpace X] {s : Set X} :
s.Nonempty → (_root_.closure s).Nonempty

Alias of the reverse direction of `closure_nonempty_iff`.

source
theorem Set.Nonempty.of_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
(_root_.closure s).Nonempty → s.Nonempty

Alias of the forward direction of `closure_nonempty_iff`.

source
theorem closure_univ {X : Type u} [TopologicalSpace X] :
closure Set.univ = Set.univ
source
theorem closure_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
closure (closure s) = closure s
source
theorem closure_eq_compl_interior_compl {X : Type u} [TopologicalSpace X] {s : Set X} :
closure s = (interior s ᶜ)ᶜ
source
@[simp]
theorem closure_union {X : Type u} [TopologicalSpace X] {s t : Set X} :
closure (s ∪ t) = closure s ∪ closure t
source
theorem Set.Finite.closure_biUnion {X : Type u} [TopologicalSpace X] {ι : Type u_1} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
source
theorem Set.Finite.closure_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : S.Finite) :
closure (⋃₀ S) = ⋃ s ∈ S, closure s
source
@[simp]
theorem Finset.closure_biUnion {X : Type u} [TopologicalSpace X] {ι : Type u_1} (s : Finset ι) (f : ι → Set X) :
closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
source
@[simp]
theorem closure_iUnion_of_finite {X : Type u} [TopologicalSpace X] {ι : Sort v} [Finite ι] (f : ι → Set X) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
source
@[simp]
theorem closure_iUnion₂_lt_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :
closure (⋃ (m : ℕ), ⋃ (_ : m < n), f m) = ⋃ (m : ℕ), ⋃ (_ : m < n), closure (f m)
source
@[simp]
theorem closure_iUnion₂_le_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :
closure (⋃ (m : ℕ), ⋃ (_ : m ≤ n), f m) = ⋃ (m : ℕ), ⋃ (_ : m ≤ n), closure (f m)
source
theorem subset_closure_inter_union_closure_compl_left {X : Type u} [TopologicalSpace X] {s t : Set X} :
closure t ⊆ closure (s ∩ t) ∪ closure s ᶜ
source
theorem subset_closure_inter_union_closure_compl_right {X : Type u} [TopologicalSpace X] {s t : Set X} :
closure s ⊆ closure (s ∩ t) ∪ closure t ᶜ
source
theorem interior_subset_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s ⊆ closure s
source
@[simp]
theorem interior_compl {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s ᶜ = (closure s)ᶜ
source
@[simp]
theorem closure_compl {X : Type u} [TopologicalSpace X] {s : Set X} :
closure s ᶜ = (interior s)ᶜ
source
theorem interior_eq_compl_closure_compl {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s = (closure s ᶜ)ᶜ
source
theorem interior_union_of_disjoint_closure {X : Type u} [TopologicalSpace X] {s t : Set X} (h : Disjoint (closure s) (closure t)) :
interior (s ∪ t) = interior s ∪ interior t
source
theorem closure_inter_of_codisjoint_interior {X : Type u} [TopologicalSpace X] {s t : Set X} (h : Codisjoint (interior s) (interior t)) :
closure (s ∩ t) = closure s ∩ closure t
source
theorem mem_closure_iff {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} :
x ∈ closure s ↔ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
source
theorem closure_inter_open_nonempty_iff {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsOpen t) :
(closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty
source
theorem Filter.le_lift'_closure {X : Type u} [TopologicalSpace X] (l : Filter X) :
l ≤ l.lift' closure
source
theorem Filter.HasBasis.lift'_closure {X : Type u} [TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) :
(l.lift' closure).HasBasis p fun (i : ι) => closure (s i)
source
theorem Filter.HasBasis.lift'_closure_eq_self {X : Type u} [TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) (hc : ∀ (i : ι), p i → IsClosed (s i)) :
l.lift' closure = l
source
@[simp]
theorem Filter.lift'_closure_eq_bot {X : Type u} [TopologicalSpace X] {l : Filter X} :
l.lift' closure = ⊥ ↔ l = ⊥
source
theorem dense_iff_closure_eq {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense s ↔ closure s = Set.univ
source
theorem Dense.closure_eq {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense s → closure s = Set.univ

Alias of the forward direction of `dense_iff_closure_eq`.

source
theorem interior_eq_empty_iff_dense_compl {X : Type u} [TopologicalSpace X] {s : Set X} :
interior s = ∅ ↔ Dense s ᶜ
source
theorem Dense.interior_compl {X : Type u} [TopologicalSpace X] {s : Set X} (h : Dense s) :
interior s ᶜ = ∅
source
@[simp]
theorem dense_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense (closure s) ↔ Dense s

The closure of a set `s` is dense if and only if `s` is dense.

source
theorem Dense.closure {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense s → Dense (closure s)

Alias of the reverse direction of `dense_closure`.

The closure of a set `s` is dense if and only if `s` is dense.

source
theorem Dense.of_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense (closure s) → Dense s

Alias of the forward direction of `dense_closure`.

The closure of a set `s` is dense if and only if `s` is dense.

source
@[simp]
theorem dense_univ {X : Type u} [TopologicalSpace X] :
Dense Set.univ
source
theorem dense_iff_inter_open {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

A set is dense if and only if it has a nonempty intersection with each nonempty open set.

source
theorem Dense.inter_open_nonempty {X : Type u} [TopologicalSpace X] {s : Set X} :
Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Alias of the forward direction of `dense_iff_inter_open`.

A set is dense if and only if it has a nonempty intersection with each nonempty open set.

source
theorem Dense.exists_mem_open {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) {U : Set X} (ho : IsOpen U) (hne : U.Nonempty) :
∃ x ∈ s, x ∈ U
source
theorem Dense.nonempty_iff {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) :
s.Nonempty ↔ Nonempty X
source
theorem Dense.nonempty {X : Type u} [TopologicalSpace X] {s : Set X} [h : Nonempty X] (hs : Dense s) :
s.Nonempty
source
theorem Dense.mono {X : Type u} [TopologicalSpace X] {s₁ s₂ : Set X} (h : s₁ ⊆ s₂) (hd : Dense s₁) :
Dense s₂
source
theorem DenseRange.of_comp {X : Type u} [TopologicalSpace X] {α : Type u_1} {β : Type u_2} {f : α → X} {g : β → α} (h : DenseRange (f ∘ g)) :
DenseRange f
source
theorem dense_compl_singleton_iff_not_open {X : Type u} [TopologicalSpace X] {x : X} :
Dense {x}ᶜ ↔ ¬IsOpen {x}

Complement to a singleton is dense if and only if the singleton is not an open set.

source
theorem Dense.induction {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) {P : X → Prop} (mem : ∀ x ∈ s, P x) (isClosed : IsClosed {x : X | P x}) (x : X) :
P x

If a closed property holds for a dense subset, it holds for the whole space.

source
theorem IsOpen.subset_interior_closure {X : Type u} [TopologicalSpace X] {s : Set X} (s_open : IsOpen s) :
s ⊆ interior (closure s)
source
theorem IsClosed.closure_interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} (s_closed : IsClosed s) :
closure (interior s) ⊆ s
source
@[simp]
theorem closure_interior_idem {X : Type u} [TopologicalSpace X] {s : Set X} :
closure (interior (closure (interior s))) = closure (interior s)
source
@[simp]
theorem interior_closure_idem {X : Type u} [TopologicalSpace X] {s : Set X} :
interior (closure (interior (closure s))) = interior (closure s)
source
@[simp]
theorem closure_diff_interior {X : Type u} [TopologicalSpace X] (s : Set X) :
closure s \ interior s = frontier s
source
theorem disjoint_interior_frontier {X : Type u} [TopologicalSpace X] {s : Set X} :
Disjoint (interior s) (frontier s)

Interior and frontier are disjoint.

source
@[simp]
theorem closure_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
closure s \ frontier s = interior s
source
@[simp]
theorem self_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
s \ frontier s = interior s
source
theorem frontier_eq_closure_inter_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
frontier s = closure s ∩ closure s ᶜ
source
theorem frontier_subset_closure {X : Type u} [TopologicalSpace X] {s : Set X} :
frontier s ⊆ closure s
source
theorem frontier_subset_iff_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} :
frontier s ⊆ s ↔ IsClosed s
source
theorem IsClosed.frontier_subset {X : Type u} [TopologicalSpace X] {s : Set X} :
IsClosed s → frontier s ⊆ s

Alias of the reverse direction of `frontier_subset_iff_isClosed`.

source
theorem frontier_closure_subset {X : Type u} [TopologicalSpace X] {s : Set X} :
frontier (closure s) ⊆ frontier s
source
theorem frontier_interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} :
frontier (interior s) ⊆ frontier s
source
@[simp]
theorem frontier_compl {X : Type u} [TopologicalSpace X] (s : Set X) :
frontier s ᶜ = frontier s

The complement of a set has the same frontier as the original set.

source
@[simp]
theorem frontier_univ {X : Type u} [TopologicalSpace X] :
frontier Set.univ = ∅
source
@[simp]
theorem frontier_empty {X : Type u} [TopologicalSpace X] :
frontier ∅ = ∅
source
theorem frontier_inter_subset {X : Type u} [TopologicalSpace X] (s t : Set X) :
frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
source
theorem frontier_union_subset {X : Type u} [TopologicalSpace X] (s t : Set X) :
frontier (s ∪ t) ⊆ frontier s ∩ closure t ᶜ ∪ closure s ᶜ ∩ frontier t
source
theorem IsClosed.frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) :
frontier s = s \ interior s
source
theorem IsOpen.frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :
frontier s = closure s \ s
source
theorem IsOpen.inter_frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :
s ∩ frontier s = ∅
source
theorem disjoint_frontier_iff_isOpen {X : Type u} [TopologicalSpace X] {s : Set X} :
Disjoint (frontier s) s ↔ IsOpen s
source
theorem isClosed_frontier {X : Type u} [TopologicalSpace X] {s : Set X} :
IsClosed (frontier s)

The frontier of a set is closed.

source
theorem interior_frontier {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsClosed s) :
interior (frontier s) = ∅

The frontier of a closed set has no interior point.

source
theorem closure_eq_interior_union_frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
closure s = interior s ∪ frontier s
source
theorem closure_eq_self_union_frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
closure s = s ∪ frontier s
source
theorem Disjoint.frontier_left {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) (hd : Disjoint s t) :
Disjoint (frontier s) t
source
theorem Disjoint.frontier_right {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (hd : Disjoint s t) :
Disjoint s (frontier t)
source
theorem frontier_eq_inter_compl_interior {X : Type u} [TopologicalSpace X] {s : Set X} :
frontier s = (interior s)ᶜ ∩ (interior s ᶜ)ᶜ
source
theorem compl_frontier_eq_union_interior {X : Type u} [TopologicalSpace X] {s : Set X} :
(frontier s)ᶜ = interior s ∪ interior s ᶜ