Documentation

Mathlib.Topology.AlexandrovDiscrete

Alexandrov-discrete topological spaces #

This file defines Alexandrov-discrete spaces, aka finitely generated spaces.

A space is Alexandrov-discrete if the (arbitrary) intersection of open sets is open. As such, the intersection of all neighborhoods of a set is a neighborhood itself. Hence every set has a minimal neighborhood, which we call the exterior of the set.

Main declarations #

Notes #

The "minimal neighborhood of a set" construction is not named in the literature. We chose the name "exterior" with analogy to the interior. interior and exterior have the same properties up to

TODO #

Finite product of Alexandrov-discrete spaces is Alexandrov-discrete.

Tags #

Alexandroff, discrete, finitely generated, fg space

A topological space is Alexandrov-discrete or finitely generated if the intersection of a family of open sets is open.

  • isOpen_sInter : ∀ (S : Set (Set α)), (sS, IsOpen s)IsOpen (⋂₀ S)

    The intersection of a family of open sets is an open set. Use isOpen_sInter in the root namespace instead.

Instances
    theorem AlexandrovDiscrete.isOpen_sInter {α : Type u_1} [TopologicalSpace α] [self : AlexandrovDiscrete α] (S : Set (Set α)) :
    (sS, IsOpen s)IsOpen (⋂₀ S)

    The intersection of a family of open sets is an open set. Use isOpen_sInter in the root namespace instead.

    Equations
    • =
    theorem isOpen_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} :
    (sS, IsOpen s)IsOpen (⋂₀ S)
    theorem isOpen_iInter {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ιSet α} (hf : ∀ (i : ι), IsOpen (f i)) :
    IsOpen (⋂ (i : ι), f i)
    theorem isOpen_iInter₂ {ι : Sort u_1} {κ : ιSort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsOpen (f i j)) :
    IsOpen (⋂ (i : ι), ⋂ (j : κ i), f i j)
    theorem isClosed_sUnion {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} (hS : sS, IsClosed s) :
    theorem isClosed_iUnion {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ιSet α} (hf : ∀ (i : ι), IsClosed (f i)) :
    IsClosed (⋃ (i : ι), f i)
    theorem isClosed_iUnion₂ {ι : Sort u_1} {κ : ιSort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsClosed (f i j)) :
    IsClosed (⋃ (i : ι), ⋃ (j : κ i), f i j)
    theorem isClopen_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} (hS : sS, IsClopen s) :
    theorem isClopen_iInter {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ιSet α} (hf : ∀ (i : ι), IsClopen (f i)) :
    IsClopen (⋂ (i : ι), f i)
    theorem isClopen_iInter₂ {ι : Sort u_1} {κ : ιSort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)) :
    IsClopen (⋂ (i : ι), ⋂ (j : κ i), f i j)
    theorem isClopen_sUnion {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} (hS : sS, IsClopen s) :
    theorem isClopen_iUnion {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ιSet α} (hf : ∀ (i : ι), IsClopen (f i)) :
    IsClopen (⋃ (i : ι), f i)
    theorem isClopen_iUnion₂ {ι : Sort u_1} {κ : ιSort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)) :
    IsClopen (⋃ (i : ι), ⋃ (j : κ i), f i j)
    theorem interior_iInter {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (f : ιSet α) :
    interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
    theorem interior_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (S : Set (Set α)) :
    interior (⋂₀ S) = sS, interior s
    theorem closure_iUnion {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (f : ιSet α) :
    closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
    theorem closure_sUnion {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (S : Set (Set α)) :
    closure (⋃₀ S) = sS, closure s
    def exterior {α : Type u_3} [TopologicalSpace α] (s : Set α) :
    Set α

    The exterior of a set is the intersection of all its neighborhoods. In an Alexandrov-discrete space, this is the smallest neighborhood of the set.

    Note that this construction is unnamed in the literature. We choose the name in analogy to interior.

    Equations
    Instances For
      theorem exterior_singleton_eq_ker_nhds {α : Type u_3} [TopologicalSpace α] (a : α) :
      exterior {a} = (nhds a).ker
      theorem exterior_def {α : Type u_3} [TopologicalSpace α] (s : Set α) :
      exterior s = ⋂₀ {t : Set α | IsOpen t s t}
      theorem mem_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} {a : α} :
      a exterior s ∀ (U : Set α), IsOpen Us Ua U
      theorem subset_exterior_iff {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} :
      s exterior t ∀ (U : Set α), IsOpen Ut Us U
      theorem subset_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} :
      theorem exterior_minimal {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (h₁ : s t) (h₂ : IsOpen t) :
      theorem IsOpen.exterior_eq {α : Type u_3} [TopologicalSpace α] {s : Set α} (h : IsOpen s) :
      theorem IsOpen.exterior_subset_iff {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) :
      theorem exterior_mono {α : Type u_3} [TopologicalSpace α] :
      Monotone exterior
      @[simp]
      @[simp]
      theorem exterior_univ {α : Type u_3} [TopologicalSpace α] :
      exterior Set.univ = Set.univ
      @[simp]
      theorem exterior_eq_empty {α : Type u_3} [TopologicalSpace α] {s : Set α} :
      @[simp]
      theorem isOpen_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} [AlexandrovDiscrete α] :
      @[simp]
      theorem exterior_subset_iff {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} [AlexandrovDiscrete α] :
      exterior s t ∃ (U : Set α), IsOpen U s U U t
      theorem IsOpen.exterior_subset {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) :
      @[simp]
      @[simp]
      theorem exterior_union {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α) (t : Set α) :
      @[simp]
      @[simp]
      theorem specializes_iff_exterior_subset {α : Type u_3} [TopologicalSpace α] {x : α} {y : α} [AlexandrovDiscrete α] :
      theorem isOpen_iff_forall_specializes {α : Type u_3} [TopologicalSpace α] {s : Set α} [AlexandrovDiscrete α] :
      IsOpen s ∀ (x y : α), x yy sx s
      theorem Set.Finite.isCompact_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} (hs : s.Finite) :
      theorem Inducing.alexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] {f : βα} (h : Inducing f) :
      theorem alexandrovDiscrete_coinduced {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {β : Type u_5} {f : αβ} :
      theorem alexandrovDiscrete_iSup {ι : Sort u_1} {α : Type u_3} {t : ιTopologicalSpace α} :
      (∀ (i : ι), AlexandrovDiscrete α)AlexandrovDiscrete α
      instance Subtype.instAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {p : αProp} :
      AlexandrovDiscrete { a : α // p a }
      Equations
      • =
      instance Sigma.instAlexandrovDiscrete {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), AlexandrovDiscrete (π i)] :
      AlexandrovDiscrete ((i : ι) × π i)
      Equations
      • =