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
• exterior: Intersection of all neighborhoods of a set. When the space is Alexandrov-discrete, this is the minimal neighborhood of the set.

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.

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

def exterior {α : Type u_3} [TopologicalSpace α] (s : Set α) : Set α

The exterior of a set is the intersection of all its neighborhoods. In an Alexandrov-discrete space, this is the smallest neighborhood of the set.

Note that this construction is unnamed in the literature. We choose the name in analogy to interior.

Equations

• exterior s = (nhdsSet s).ker

theorem exterior_singleton_eq_ker_nhds {α : Type u_3} [TopologicalSpace α] (a : α) : exterior {a} = (nhds a).ker

@[simp]

theorem mem_exterior_singleton {α : Type u_3} [TopologicalSpace α] {x : α} {y : α} : x ∈ exterior {y} ↔ x ⤳ y

theorem exterior_def {α : Type u_3} [TopologicalSpace α] (s : Set α) : exterior s = ⋂₀ {t : Set α | IsOpen t ∧ s ⊆ t}

theorem mem_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ exterior s ↔ ∀ (U : Set α), IsOpen U → s ⊆ U → a ∈ U

theorem subset_exterior_iff {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} : s ⊆ exterior t ↔ ∀ (U : Set α), IsOpen U → t ⊆ U → s ⊆ U

theorem subset_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} : s ⊆ exterior s

theorem exterior_minimal {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t

theorem IsOpen.exterior_eq {α : Type u_3} [TopologicalSpace α] {s : Set α} (h : IsOpen s) : exterior s = s

theorem IsOpen.exterior_subset {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t

@[deprecated IsOpen.exterior_subset]

theorem IsOpen.exterior_subset_iff {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t

Alias of IsOpen.exterior_subset.

@[simp]

theorem exterior_iUnion {α : Type u_3} [TopologicalSpace α] {ι : Sort u_5} (s : ι → Set α) : exterior (⋃ (i : ι), s i) = ⋃ (i : ι), exterior (s i)

@[simp]

theorem exterior_union {α : Type u_3} [TopologicalSpace α] (s : Set α) (t : Set α) : exterior (s ∪ t) = exterior s ∪ exterior t

@[simp]

theorem exterior_sUnion {α : Type u_3} [TopologicalSpace α] (S : Set (Set α)) : exterior (⋃₀ S) = ⋃ s ∈ S, exterior s

theorem mem_exterior_iff_specializes {α : Type u_3} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ exterior s ↔ ∃ b ∈ s, a ⤳ b

theorem exterior_mono {α : Type u_3} [TopologicalSpace α] : Monotone exterior

theorem exterior_subset_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} (h : s ⊆ t) : exterior s ⊆ exterior t

This name was used to be used for the Iff version, see exterior_subset_exterior_iff_nhdsSet.

@[simp]

theorem exterior_subset_exterior_iff_nhdsSet {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} : exterior s ⊆ exterior t ↔ nhdsSet s ≤ nhdsSet t

theorem exterior_eq_exterior_iff_nhdsSet {α : Type u_3} [TopologicalSpace α] {s : Set α} {t : Set α} : exterior s = exterior t ↔ nhdsSet s = nhdsSet t

theorem specializes_iff_exterior_subset {α : Type u_3} [TopologicalSpace α] {x : α} {y : α} : x ⤳ y ↔ exterior {x} ⊆ exterior {y}

@[simp]

theorem exterior_empty {α : Type u_3} [TopologicalSpace α] : exterior ∅ = ∅

@[simp]

theorem exterior_univ {α : Type u_3} [TopologicalSpace α] : exterior Set.univ = Set.univ

@[simp]

theorem exterior_eq_empty {α : Type u_3} [TopologicalSpace α] {s : Set α} : exterior s = ∅ ↔ s = ∅

@[simp]

theorem nhdsSet_exterior {α : Type u_3} [TopologicalSpace α] (s : Set α) : nhdsSet (exterior s) = nhdsSet s

@[simp]

theorem exterior_exterior {α : Type u_3} [TopologicalSpace α] (s : Set α) : exterior (exterior s) = exterior s

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

theorem IsCompact.exterior_iff {α : Type u_3} [TopologicalSpace α] {s : Set α} : IsCompact (exterior s) ↔ IsCompact s

theorem IsCompact.exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} : IsCompact s → IsCompact (exterior s)

Alias of the reverse direction of IsCompact.exterior_iff.

theorem IsCompact.of_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} : IsCompact (exterior s) → IsCompact s

Alias of the forward direction of IsCompact.exterior_iff.

@[deprecated IsCompact.exterior]

theorem Set.Finite.isCompact_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} (hs : s.Finite) : IsCompact (exterior s)

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

• ⋯ = ⋯