Openness and closedness of a set

This file provides lemmas relating to the predicates IsOpen and IsClosed of a set endowed with a topology.

Implementation notes

Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in https://leanprover-community.github.io/theories/topology.html.

References

• [N. Bourbaki, General Topology][bourbaki1966]
• [I. M. James, Topologies and Uniformities][james1999]

Tags

topological space

def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : ∅ ∈ T) (sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T) (union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T) : TopologicalSpace X

A constructor for topologies by specifying the closed sets, and showing that they satisfy the appropriate conditions.

Equations

• TopologicalSpace.ofClosed T empty_mem sInter_mem union_mem = { IsOpen := fun (X_1 : Set X) => X_1ᶜ ∈ T, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem isOpen_mk {X : Type u} {s : Set X} {p : Set X → Prop} {h₁ : p Set.univ} {h₂ : ∀ (s t : Set X), p s → p t → p (s ∩ t)} {h₃ : ∀ (s : Set (Set X)), (∀ t ∈ s, p t) → p (⋃₀ s)} : IsOpen s ↔ p s

theorem TopologicalSpace.ext {X : Type u} {f g : TopologicalSpace X} : IsOpen = IsOpen → f = g

theorem TopologicalSpace.ext_iff {X : Type u} {t t' : TopologicalSpace X} : t = t' ↔ ∀ (s : Set X), IsOpen s ↔ IsOpen s

theorem isOpen_fold {X : Type u} {s : Set X} {t : TopologicalSpace X} : TopologicalSpace.IsOpen s = IsOpen s

theorem isOpen_iUnion {X : Type u} {ι : Sort v} [TopologicalSpace X] {f : ι → Set X} (h : ∀ (i : ι), IsOpen (f i)) : IsOpen (⋃ (i : ι), f i)

theorem isOpen_biUnion {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋃ i ∈ s, f i)

theorem IsOpen.union {X : Type u} {s₁ s₂ : Set X} [TopologicalSpace X] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂)

theorem isOpen_iff_of_cover {X : Type u} {α : Type u_1} {s : Set X} [TopologicalSpace X] {f : α → Set X} (ho : ∀ (i : α), IsOpen (f i)) (hU : ⋃ (i : α), f i = Set.univ) : IsOpen s ↔ ∀ (i : α), IsOpen (f i ∩ s)

@[simp]

theorem isOpen_empty {X : Type u} [TopologicalSpace X] : IsOpen ∅

theorem Set.Finite.isOpen_sInter {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (hs : s.Finite) (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋂₀ s)

theorem Set.Finite.isOpen_biInter {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i)

theorem isOpen_iInter_of_finite {X : Type u} {ι : Sort v} [TopologicalSpace X] [Finite ι] {s : ι → Set X} (h : ∀ (i : ι), IsOpen (s i)) : IsOpen (⋂ (i : ι), s i)

theorem isOpen_biInter_finset {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i)

@[simp]

theorem isOpen_const {X : Type u} [TopologicalSpace X] {p : Prop} : IsOpen {_x : X | p}

theorem IsOpen.and {X : Type u} {p₁ p₂ : X → Prop} [TopologicalSpace X] : IsOpen {x : X | p₁ x} → IsOpen {x : X | p₂ x} → IsOpen {x : X | p₁ x ∧ p₂ x}

@[simp]

theorem isOpen_compl_iff {X : Type u} {s : Set X} [TopologicalSpace X] : IsOpen sᶜ ↔ IsClosed s

theorem TopologicalSpace.ext_iff_isClosed {X : Type u_2} {t₁ t₂ : TopologicalSpace X} : t₁ = t₂ ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s

theorem TopologicalSpace.ext_isClosed {X : Type u_2} {t₁ t₂ : TopologicalSpace X} : (∀ (s : Set X), IsClosed s ↔ IsClosed s) → t₁ = t₂

Alias of the reverse direction of TopologicalSpace.ext_iff_isClosed.

theorem isClosed_const {X : Type u} [TopologicalSpace X] {p : Prop} : IsClosed {_x : X | p}

@[simp]

theorem isClosed_empty {X : Type u} [TopologicalSpace X] : IsClosed ∅

@[simp]

theorem isClosed_univ {X : Type u} [TopologicalSpace X] : IsClosed Set.univ

theorem IsOpen.isLocallyClosed {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) : IsLocallyClosed s

theorem IsClosed.isLocallyClosed {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) : IsLocallyClosed s

theorem IsClosed.union {X : Type u} {s₁ s₂ : Set X} [TopologicalSpace X] : IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)

theorem isClosed_sInter {X : Type u} [TopologicalSpace X] {s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)

theorem isClosed_iInter {X : Type u} {ι : Sort v} [TopologicalSpace X] {f : ι → Set X} (h : ∀ (i : ι), IsClosed (f i)) : IsClosed (⋂ (i : ι), f i)

theorem isClosed_biInter {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋂ i ∈ s, f i)

@[simp]

theorem isClosed_compl_iff {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed sᶜ ↔ IsOpen s

theorem IsOpen.isClosed_compl {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s → IsClosed sᶜ

Alias of the reverse direction of isClosed_compl_iff.

theorem IsOpen.sdiff {X : Type u} {s t : Set X} [TopologicalSpace X] (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t)

theorem IsClosed.inter {X : Type u} {s₁ s₂ : Set X} [TopologicalSpace X] (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ∩ s₂)

theorem IsClosed.sdiff {X : Type u} {s t : Set X} [TopologicalSpace X] (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t)

theorem Set.Finite.isClosed_biUnion {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋃ i ∈ s, f i)

theorem isClosed_biUnion_finset {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋃ i ∈ s, f i)

theorem isClosed_iUnion_of_finite {X : Type u} {ι : Sort v} [TopologicalSpace X] [Finite ι] {s : ι → Set X} (h : ∀ (i : ι), IsClosed (s i)) : IsClosed (⋃ (i : ι), s i)

theorem isClosed_imp {X : Type u} [TopologicalSpace X] {p q : X → Prop} (hp : IsOpen {x : X | p x}) (hq : IsClosed {x : X | q x}) : IsClosed {x : X | p x → q x}

theorem IsClosed.not {X : Type u} {p : X → Prop} [TopologicalSpace X] : IsClosed {a : X | p a} → IsOpen {a : X | ¬p a}

Limits of filters in topological spaces

In this section we define functions that return a limit of a filter (or of a function along a filter), if it exists, and a random point otherwise. These functions are rarely used in Mathlib, most of the theorems are written using Filter.Tendsto. One of the reasons is that Filter.limUnder f g = x is not equivalent to Filter.Tendsto g f (𝓝 x) unless the codomain is a Hausdorff space and g has a limit along f.

theorem le_nhds_lim {X : Type u} [TopologicalSpace X] {f : Filter X} (h : ∃ (x : X), f ≤ nhds x) : f ≤ nhds (lim f)

If a filter f is majorated by some 𝓝 x, then it is majorated by 𝓝 (Filter.lim f). We formulate this lemma with a [Nonempty X] argument of lim derived from h to make it useful for types without a [Nonempty X] instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance.

theorem tendsto_nhds_limUnder {X : Type u} {α : Type u_1} [TopologicalSpace X] {f : Filter α} {g : α → X} (h : ∃ (x : X), Filter.Tendsto g f (nhds x)) : Filter.Tendsto g f (nhds (limUnder f g))

If g tends to some 𝓝 x along f, then it tends to 𝓝 (Filter.limUnder f g). We formulate this lemma with a [Nonempty X] argument of lim derived from h to make it useful for types without a [Nonempty X] instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance.

theorem limUnder_of_not_tendsto {X : Type u} {α : Type u_1} [TopologicalSpace X] [hX : Nonempty X] {f : Filter α} {g : α → X} (h : ¬∃ (x : X), Filter.Tendsto g f (nhds x)) : limUnder f g = Classical.choice hX