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

theorem mem_interior {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

@[simp]

theorem isOpen_interior {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen (interior s)

theorem interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} : interior s ⊆ s

theorem interior_maximal {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s

theorem IsOpen.interior_eq {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsOpen s) : interior s = s

theorem interior_eq_iff_isOpen {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = s ↔ IsOpen s

theorem subset_interior_iff_isOpen {X : Type u} [TopologicalSpace X] {s : Set X} : s ⊆ interior s ↔ IsOpen s

theorem IsOpen.subset_interior_iff {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t

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

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

theorem interior_mono {X : Type u} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) : interior s ⊆ interior t

@[simp]

theorem interior_empty {X : Type u} [TopologicalSpace X] : interior ∅ = ∅

@[simp]

theorem interior_univ {X : Type u} [TopologicalSpace X] : interior Set.univ = Set.univ

@[simp]

theorem interior_eq_univ {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = Set.univ ↔ s = Set.univ

@[simp]

theorem interior_interior {X : Type u} [TopologicalSpace X] {s : Set X} : interior (interior s) = interior s

@[simp]

theorem interior_inter {X : Type u} [TopologicalSpace X] {s t : Set X} : interior (s ∩ t) = interior s ∩ interior t

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)

theorem Set.Finite.interior_sInter {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : S.Finite) : interior (⋂₀ S) = ⋂ s ∈ S, interior s

@[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)

@[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)

@[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)

@[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)

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

theorem isOpen_iff_forall_mem_open {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

theorem interior_iInter_subset {X : Type u} [TopologicalSpace X] {ι : Sort v} (s : ι → Set X) : interior (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), interior (s i)

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)

theorem interior_sInter_subset {X : Type u} [TopologicalSpace X] (S : Set (Set X)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s

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)

theorem Filter.lift'_interior_le {X : Type u} [TopologicalSpace X] (l : Filter X) : l.lift' interior ≤ l

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

@[simp]

theorem isClosed_closure {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed (closure s)

theorem subset_closure {X : Type u} [TopologicalSpace X] {s : Set X} : s ⊆ closure s

theorem not_mem_of_not_mem_closure {X : Type u} [TopologicalSpace X] {s : Set X} {P : X} (hP : P ∉ closure s) : P ∉ s

theorem closure_minimal {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : s ⊆ t) (h₂ : IsClosed t) : closure s ⊆ t

theorem Disjoint.closure_left {X : Type u} [TopologicalSpace X] {s t : Set X} (hd : Disjoint s t) (ht : IsOpen t) : Disjoint (closure s) t

theorem Disjoint.closure_right {X : Type u} [TopologicalSpace X] {s t : Set X} (hd : Disjoint s t) (hs : IsOpen s) : Disjoint s (closure t)

@[simp]

theorem IsClosed.closure_eq {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsClosed s) : closure s = s

theorem IsClosed.closure_subset {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : closure s ⊆ s

theorem IsClosed.closure_subset_iff {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : IsClosed t) : closure s ⊆ t ↔ s ⊆ t

theorem IsClosed.mem_iff_closure_subset {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsClosed s) : x ∈ s ↔ closure {x} ⊆ s

theorem closure_mono {X : Type u} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) : closure s ⊆ closure t

theorem monotone_closure (X : Type u_1) [TopologicalSpace X] : Monotone closure

theorem diff_subset_closure_iff {X : Type u} [TopologicalSpace X] {s t : Set X} : s \ t ⊆ closure t ↔ s ⊆ closure t

theorem closure_inter_subset_inter_closure {X : Type u} [TopologicalSpace X] (s t : Set X) : closure (s ∩ t) ⊆ closure s ∩ closure t

theorem isClosed_of_closure_subset {X : Type u} [TopologicalSpace X] {s : Set X} (h : closure s ⊆ s) : IsClosed s

theorem closure_eq_iff_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} : closure s = s ↔ IsClosed s

theorem closure_subset_iff_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} : closure s ⊆ s ↔ IsClosed s

theorem closure_empty {X : Type u} [TopologicalSpace X] : closure ∅ = ∅

@[simp]

theorem closure_empty_iff {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = ∅ ↔ s = ∅

@[simp]

theorem closure_nonempty_iff {X : Type u} [TopologicalSpace X] {s : Set X} : (closure s).Nonempty ↔ s.Nonempty

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.

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.

theorem closure_univ {X : Type u} [TopologicalSpace X] : closure Set.univ = Set.univ

theorem closure_closure {X : Type u} [TopologicalSpace X] {s : Set X} : closure (closure s) = closure s

theorem closure_eq_compl_interior_compl {X : Type u} [TopologicalSpace X] {s : Set X} : closure s = (interior sᶜ)ᶜ

@[simp]

theorem closure_union {X : Type u} [TopologicalSpace X] {s t : Set X} : closure (s ∪ t) = closure s ∪ closure t

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)

theorem Set.Finite.closure_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : S.Finite) : closure (⋃₀ S) = ⋃ s ∈ S, closure s

@[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)

@[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)

@[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)

@[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)

theorem interior_subset_closure {X : Type u} [TopologicalSpace X] {s : Set X} : interior s ⊆ closure s

@[simp]

theorem interior_compl {X : Type u} [TopologicalSpace X] {s : Set X} : interior sᶜ = (closure s)ᶜ

@[simp]

theorem closure_compl {X : Type u} [TopologicalSpace X] {s : Set X} : closure sᶜ = (interior s)ᶜ

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

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

theorem Filter.le_lift'_closure {X : Type u} [TopologicalSpace X] (l : Filter X) : l ≤ l.lift' closure

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)

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

@[simp]

theorem Filter.lift'_closure_eq_bot {X : Type u} [TopologicalSpace X] {l : Filter X} : l.lift' closure = ⊥ ↔ l = ⊥

theorem dense_iff_closure_eq {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s ↔ closure s = Set.univ

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.

theorem interior_eq_empty_iff_dense_compl {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = ∅ ↔ Dense sᶜ

theorem Dense.interior_compl {X : Type u} [TopologicalSpace X] {s : Set X} (h : Dense s) : interior sᶜ = ∅

@[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.

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.

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.

@[simp]

theorem dense_univ {X : Type u} [TopologicalSpace X] : Dense Set.univ

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.

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.

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

theorem Dense.nonempty_iff {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) : s.Nonempty ↔ Nonempty X

theorem Dense.nonempty {X : Type u} [TopologicalSpace X] {s : Set X} [h : Nonempty X] (hs : Dense s) : s.Nonempty

theorem Dense.mono {X : Type u} [TopologicalSpace X] {s₁ s₂ : Set X} (h : s₁ ⊆ s₂) (hd : Dense s₁) : Dense s₂

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.

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.

theorem IsOpen.subset_interior_closure {X : Type u} [TopologicalSpace X] {s : Set X} (s_open : IsOpen s) : s ⊆ interior (closure s)

theorem IsClosed.closure_interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} (s_closed : IsClosed s) : closure (interior s) ⊆ s

@[simp]

theorem closure_diff_interior {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ interior s = frontier s

theorem disjoint_interior_frontier {X : Type u} [TopologicalSpace X] {s : Set X} : Disjoint (interior s) (frontier s)

Interior and frontier are disjoint.

@[simp]

theorem closure_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ frontier s = interior s

@[simp]

theorem self_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : s \ frontier s = interior s

theorem frontier_eq_closure_inter_closure {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s = closure s ∩ closure sᶜ

theorem frontier_subset_closure {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s ⊆ closure s

theorem frontier_subset_iff_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s ⊆ s ↔ IsClosed s

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.

theorem frontier_closure_subset {X : Type u} [TopologicalSpace X] {s : Set X} : frontier (closure s) ⊆ frontier s

theorem frontier_interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} : frontier (interior s) ⊆ frontier s

@[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.

@[simp]

theorem frontier_univ {X : Type u} [TopologicalSpace X] : frontier Set.univ = ∅

@[simp]

theorem frontier_empty {X : Type u} [TopologicalSpace X] : frontier ∅ = ∅

theorem frontier_inter_subset {X : Type u} [TopologicalSpace X] (s t : Set X) : frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

theorem frontier_union_subset {X : Type u} [TopologicalSpace X] (s t : Set X) : frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

theorem IsClosed.frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : frontier s = s \ interior s

theorem IsOpen.frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : frontier s = closure s \ s

theorem IsOpen.inter_frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : s ∩ frontier s = ∅

theorem disjoint_frontier_iff_isOpen {X : Type u} [TopologicalSpace X] {s : Set X} : Disjoint (frontier s) s ↔ IsOpen s

theorem isClosed_frontier {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed (frontier s)

The frontier of a set is closed.

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.

theorem closure_eq_interior_union_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = interior s ∪ frontier s

theorem closure_eq_self_union_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = s ∪ frontier s

theorem Disjoint.frontier_left {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) (hd : Disjoint s t) : Disjoint (frontier s) t

theorem Disjoint.frontier_right {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (hd : Disjoint s t) : Disjoint s (frontier t)

theorem frontier_eq_inter_compl_interior {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ

theorem compl_frontier_eq_union_interior {X : Type u} [TopologicalSpace X] {s : Set X} : (frontier s)ᶜ = interior s ∪ interior sᶜ