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 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
    @[deprecated Topology.IsInducing.alexandrovDiscrete]

    Alias of Topology.IsInducing.alexandrovDiscrete.

    theorem alexandrovDiscrete_iSup {ι : Sort u_1} {α : Type u_3} {t : ιTopologicalSpace α} :
    (∀ (i : ι), AlexandrovDiscrete α)AlexandrovDiscrete α
    @[simp]
    theorem isOpen_exterior {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
    @[simp]
    theorem exterior_subset_iff {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :
    exterior s t ∃ (U : Set α), IsOpen U s U U t
    theorem isOpen_iff_forall_specializes {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
    IsOpen s ∀ (x y : α), x yy sx s
    theorem alexandrovDiscrete_coinduced {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {β : Type u_5} {f : αβ} :
    theorem Subtype.instAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {p : αProp} :
    AlexandrovDiscrete { a : α // p a }
    theorem Sigma.instAlexandrovDiscrete {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), AlexandrovDiscrete (π i)] :
    AlexandrovDiscrete ((i : ι) × π i)