# 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 neighborhoods kernel of the set.

## Main declarations #

- `AlexandrovDiscrete`: Prop-valued typeclass for a topological space to be Alexandrov-discrete

## Tags #

Alexandroff, discrete, finitely generated, fg space

source
class AlexandrovDiscrete (α : Type u_1) [TopologicalSpace α] :
Prop

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 α)) : (∀ s ∈ S, 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

source
theorem alexandrovDiscrete_iff (α : Type u_1) [TopologicalSpace α] :
AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
source
theorem alexandrovDiscrete_iff_isClosed {α : Type u_3} [TopologicalSpace α] :
AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S)
source
instance DiscreteTopology.toAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [DiscreteTopology α] :
AlexandrovDiscrete α
source
instance Finite.toAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [Finite α] :
AlexandrovDiscrete α
source
theorem isOpen_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} :
(∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
source
theorem isOpen_iInter {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α} (hf : ∀ (i : ι), IsOpen (f i)) :
IsOpen (⋂ (i : ι), f i)
source
theorem isOpen_iInter₂ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsOpen (f i j)) :
IsOpen (⋂ (i : ι), ⋂ (j : κ i), f i j)
source
theorem isClosed_sUnion {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} (hS : ∀ s ∈ S, IsClosed s) :
IsClosed (⋃₀ S)
source
theorem isClosed_iUnion {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α} (hf : ∀ (i : ι), IsClosed (f i)) :
IsClosed (⋃ (i : ι), f i)
source
theorem isClosed_iUnion₂ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsClosed (f i j)) :
IsClosed (⋃ (i : ι), ⋃ (j : κ i), f i j)
source
theorem isClopen_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} (hS : ∀ s ∈ S, IsClopen s) :
IsClopen (⋂₀ S)
source
theorem isClopen_iInter {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α} (hf : ∀ (i : ι), IsClopen (f i)) :
IsClopen (⋂ (i : ι), f i)
source
theorem isClopen_iInter₂ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)) :
IsClopen (⋂ (i : ι), ⋂ (j : κ i), f i j)
source
theorem isClopen_sUnion {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} (hS : ∀ s ∈ S, IsClopen s) :
IsClopen (⋃₀ S)
source
theorem isClopen_iUnion {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α} (hf : ∀ (i : ι), IsClopen (f i)) :
IsClopen (⋃ (i : ι), f i)
source
theorem isClopen_iUnion₂ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsClopen (f i j)) :
IsClopen (⋃ (i : ι), ⋃ (j : κ i), f i j)
source
theorem interior_iInter {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (f : ι → Set α) :
interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
source
theorem interior_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (S : Set (Set α)) :
interior (⋂₀ S) = ⋂ s ∈ S, interior s
source
theorem closure_iUnion {ι : Sort u_1} {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (f : ι → Set α) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
source
theorem closure_sUnion {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (S : Set (Set α)) :
closure (⋃₀ S) = ⋃ s ∈ S, closure s
source
theorem Topology.IsInducing.alexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] {f : β → α} (h : IsInducing f) :
AlexandrovDiscrete β
source
theorem AlexandrovDiscrete.sup {α : Type u_3} {t₁ t₂ : TopologicalSpace α} :
AlexandrovDiscrete α → AlexandrovDiscrete α → AlexandrovDiscrete α
source
theorem alexandrovDiscrete_iSup {ι : Sort u_1} {α : Type u_3} {t : ι → TopologicalSpace α} :
(∀ (i : ι), AlexandrovDiscrete α) → AlexandrovDiscrete α
source
@[simp]
theorem isOpen_nhdsKer {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
IsOpen (nhdsKer s)
source
@[deprecated isOpen_nhdsKer (since := "2025-07-09")]
theorem isOpen_exterior {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
IsOpen (nhdsKer s)

Alias of `isOpen_nhdsKer`.

source
theorem nhdsKer_mem_nhdsSet {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
nhdsKer s ∈ nhdsSet s
source
@[deprecated nhdsKer_mem_nhdsSet (since := "2025-07-09")]
theorem exterior_mem_nhdsSet {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
nhdsKer s ∈ nhdsSet s

Alias of `nhdsKer_mem_nhdsSet`.

source
@[simp]
theorem nhdsKer_eq_iff_isOpen {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
nhdsKer s = s ↔ IsOpen s
source
@[deprecated nhdsKer_eq_iff_isOpen (since := "2025-07-09")]
theorem exterior_eq_iff_isOpen {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
nhdsKer s = s ↔ IsOpen s

Alias of `nhdsKer_eq_iff_isOpen`.

source
@[simp]
theorem nhdsKer_subset_iff_isOpen {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
nhdsKer s ⊆ s ↔ IsOpen s
source
@[deprecated nhdsKer_subset_iff_isOpen (since := "2025-07-09")]
theorem exterior_subset_iff_isOpen {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
nhdsKer s ⊆ s ↔ IsOpen s

Alias of `nhdsKer_subset_iff_isOpen`.

source
theorem nhdsKer_subset_iff {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :
nhdsKer s ⊆ t ↔ ∃ (U : Set α), IsOpen U ∧ s ⊆ U ∧ U ⊆ t
source
@[deprecated nhdsKer_subset_iff (since := "2025-07-09")]
theorem exterior_subset_iff {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :
nhdsKer s ⊆ t ↔ ∃ (U : Set α), IsOpen U ∧ s ⊆ U ∧ U ⊆ t

Alias of `nhdsKer_subset_iff`.

source
theorem nhdsKer_subset_iff_mem_nhdsSet {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :
nhdsKer s ⊆ t ↔ t ∈ nhdsSet s
source
@[deprecated nhdsKer_subset_iff_mem_nhdsSet (since := "2025-07-09")]
theorem exterior_subset_iff_mem_nhdsSet {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :
nhdsKer s ⊆ t ↔ t ∈ nhdsSet s

Alias of `nhdsKer_subset_iff_mem_nhdsSet`.

source
theorem nhdsKer_singleton_subset_iff_mem_nhds {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {t : Set α} {a : α} :
nhdsKer {a} ⊆ t ↔ t ∈ nhds a
source
@[deprecated nhdsKer_singleton_subset_iff_mem_nhds (since := "2025-07-09")]
theorem exterior_singleton_subset_iff_mem_nhds {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {t : Set α} {a : α} :
nhdsKer {a} ⊆ t ↔ t ∈ nhds a

Alias of `nhdsKer_singleton_subset_iff_mem_nhds`.

source
theorem gc_nhdsKer_interior {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :
GaloisConnection nhdsKer interior
source
@[deprecated gc_nhdsKer_interior (since := "2025-07-09")]
theorem gc_exterior_interior {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :
GaloisConnection nhdsKer interior

Alias of `gc_nhdsKer_interior`.

source
@[simp]
theorem principal_nhdsKer {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α) :
Filter.principal (nhdsKer s) = nhdsSet s
source
@[deprecated principal_nhdsKer (since := "2025-07-09")]
theorem principal_exterior {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α) :
Filter.principal (nhdsKer s) = nhdsSet s

Alias of `principal_nhdsKer`.

source
theorem principal_nhdsKer_singleton {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (a : α) :
Filter.principal (nhdsKer {a}) = nhds a
source
theorem nhdsSet_basis_nhdsKer {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α) :
(nhdsSet s).HasBasis (fun (x : Unit) => True) fun (x : Unit) => nhdsKer s
source
theorem nhds_basis_nhdsKer_singleton {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (a : α) :
(nhds a).HasBasis (fun (x : Unit) => True) fun (x : Unit) => nhdsKer {a}
source
theorem isOpen_iff_forall_specializes {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s
source
theorem alexandrovDiscrete_iff_nhds {α : Type u_3} [TopologicalSpace α] :
AlexandrovDiscrete α ↔ ∀ (a : α), nhds a = Filter.principal (nhdsKer {a})
source
theorem alexandrovDiscrete_coinduced {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {β : Type u_5} {f : α → β} :
AlexandrovDiscrete β
source
instance AlexandrovDiscrete.toFirstCountable {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :
FirstCountableTopology α
source
instance AlexandrovDiscrete.toLocallyCompactSpace {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :
LocallyCompactSpace α
source
instance Subtype.instAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {p : α → Prop} :
AlexandrovDiscrete { a : α // p a }
source
instance Quotient.instAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Setoid α} :
AlexandrovDiscrete (Quotient s)
source
instance Sum.instAlexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] [AlexandrovDiscrete β] :
AlexandrovDiscrete (α ⊕ β)
source
instance Sigma.instAlexandrovDiscrete {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), AlexandrovDiscrete (X i)] :
AlexandrovDiscrete ((i : ι) × X i)
source
instance Prod.instAlexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] [AlexandrovDiscrete β] :
AlexandrovDiscrete (α × β)
source
instance Pi.instAlexandrovDiscreteOfFinite {ι : Type u_5} [Finite ι] {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), AlexandrovDiscrete (X i)] :
AlexandrovDiscrete ((i : ι) → X i)