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 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

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

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

theorem alexandrovDiscrete_iff (α : Type u_1) [TopologicalSpace α] :

AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)

theorem alexandrovDiscrete_iff_isClosed {α : Type u_3} [TopologicalSpace α] :

AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S)

instance DiscreteTopology.toAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [DiscreteTopology α] :

AlexandrovDiscrete α

instance Finite.toAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [Finite α] :

AlexandrovDiscrete α

theorem isOpen_sInter {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)} :

(∀ s ∈ S, 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 : ι) → κ i → Set α} (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 : ∀ s ∈ S, IsClosed s) :

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 : ι) → κ i → Set α} (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 : ∀ s ∈ S, IsClopen s) :

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 : ι) → κ i → Set α} (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 : ∀ s ∈ S, IsClopen s) :

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 : ι) → κ i → Set α} (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) = ⋂ s ∈ S, 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) = ⋃ s ∈ S, closure s

theorem Topology.IsInducing.alexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] {f : β → α} (h : IsInducing f) :

AlexandrovDiscrete β

theorem AlexandrovDiscrete.sup {α : Type u_3} {t₁ t₂ : TopologicalSpace α} :

AlexandrovDiscrete α → AlexandrovDiscrete α → AlexandrovDiscrete α

theorem alexandrovDiscrete_iSup {ι : Sort u_1} {α : Type u_3} {t : ι → TopologicalSpace α} :

(∀ (i : ι), AlexandrovDiscrete α) → AlexandrovDiscrete α

@[simp]

theorem isOpen_nhdsKer {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :

IsOpen (nhdsKer s)

theorem nhdsKer_mem_nhdsSet {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :

nhdsKer s ∈ nhdsSet s

@[simp]

theorem nhdsKer_eq_iff_isOpen {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :

nhdsKer s = s ↔ IsOpen s

@[simp]

theorem nhdsKer_subset_iff_isOpen {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :

nhdsKer s ⊆ s ↔ IsOpen s

theorem nhdsKer_subset_iff {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :

nhdsKer s ⊆ t ↔ ∃ (U : Set α), IsOpen U ∧ s ⊆ U ∧ U ⊆ t

theorem nhdsKer_subset_iff_mem_nhdsSet {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s t : Set α} :

nhdsKer s ⊆ t ↔ t ∈ nhdsSet s

theorem nhdsKer_singleton_subset_iff_mem_nhds {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {t : Set α} {a : α} :

nhdsKer {a} ⊆ t ↔ t ∈ nhds a

theorem gc_nhdsKer_interior {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :

GaloisConnection nhdsKer interior

@[simp]

theorem principal_nhdsKer {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α) :

Filter.principal (nhdsKer s) = nhdsSet s

theorem principal_nhdsKer_singleton {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (a : α) :

Filter.principal (nhdsKer {a}) = nhds a

theorem nhdsSet_basis_nhdsKer {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α) :

(nhdsSet s).HasBasis (fun (x : Unit) => True) fun (x : Unit) => nhdsKer s

theorem nhds_basis_nhdsKer_singleton {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] (a : α) :

(nhds a).HasBasis (fun (x : Unit) => True) fun (x : Unit) => nhdsKer {a}

theorem isOpen_iff_forall_specializes {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :

IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s

theorem alexandrovDiscrete_iff_nhds {α : Type u_3} [TopologicalSpace α] :

AlexandrovDiscrete α ↔ ∀ (a : α), nhds a = Filter.principal (nhdsKer {a})

theorem alexandrovDiscrete_coinduced {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {β : Type u_5} {f : α → β} :

AlexandrovDiscrete β

instance AlexandrovDiscrete.toFirstCountable {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :

FirstCountableTopology α

instance AlexandrovDiscrete.toLocallyCompactSpace {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] :

LocallyCompactSpace α

instance Subtype.instAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {p : α → Prop} :

AlexandrovDiscrete { a : α // p a }

instance Quotient.instAlexandrovDiscrete {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Setoid α} :

AlexandrovDiscrete (Quotient s)

instance Sum.instAlexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] [AlexandrovDiscrete β] :

AlexandrovDiscrete (α ⊕ β)

instance Sigma.instAlexandrovDiscrete {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), AlexandrovDiscrete (X i)] :

AlexandrovDiscrete ((i : ι) × X i)

instance Prod.instAlexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] [AlexandrovDiscrete β] :

AlexandrovDiscrete (α × β)

instance Pi.instAlexandrovDiscreteOfFinite {ι : Type u_5} [Finite ι] {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), AlexandrovDiscrete (X i)] :

AlexandrovDiscrete ((i : ι) → X i)