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 α] : 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.

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

@[deprecated Topology.IsInducing.alexandrovDiscrete]

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

Alias of Topology.IsInducing.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_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 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 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

• ⋯ = ⋯