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 #

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

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

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.isOpen_sInter {α : Type u_1} :

∀ {inst : TopologicalSpace α} [self : AlexandrovDiscrete α] (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.

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

AlexandrovDiscrete α

Equations

⋯ = ⋯

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

AlexandrovDiscrete α

Equations

⋯ = ⋯

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 IsInducing.alexandrovDiscrete {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [AlexandrovDiscrete α] {f : β → α} (h : IsInducing f) :

AlexandrovDiscrete β

@[deprecated IsInducing.alexandrovDiscrete]

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

AlexandrovDiscrete β

Alias of IsInducing.alexandrovDiscrete.

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

AlexandrovDiscrete α → AlexandrovDiscrete α → 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 α} :

IsOpen (exterior s)

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

exterior s ∈ nhdsSet s

@[simp]

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

exterior s = s ↔ IsOpen s

@[simp]

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

exterior s ⊆ s ↔ IsOpen s

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

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

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

exterior s ⊆ t ↔ t ∈ nhdsSet s

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

exterior {a} ⊆ t ↔ t ∈ nhds a

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

GaloisConnection exterior interior

@[simp]

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

Filter.principal (exterior s) = nhdsSet s

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

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

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

AlexandrovDiscrete β

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

FirstCountableTopology α

Equations

⋯ = ⋯

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

LocallyCompactSpace α

Equations

⋯ = ⋯

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

AlexandrovDiscrete { a : α // p a }

Equations

⋯ = ⋯

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

AlexandrovDiscrete (Quotient s)

Equations

⋯ = ⋯

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

AlexandrovDiscrete (α ⊕ β)

Equations

⋯ = ⋯

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

AlexandrovDiscrete ((i : ι) × π i)

Equations

⋯ = ⋯