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

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

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

AlexandrovDiscrete α

Equations

(_ : AlexandrovDiscrete α) = (_ : AlexandrovDiscrete α)

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

AlexandrovDiscrete α

Equations

(_ : AlexandrovDiscrete α) = (_ : 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

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 = Filter.ker (nhdsSet s)

Instances For

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

exterior {a} = Filter.ker (nhds a)

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

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

exterior s ⊆ t ↔ s ⊆ t

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

Monotone exterior

@[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 isOpen_exterior {α : Type u_3} [TopologicalSpace α] {s : Set α} [AlexandrovDiscrete α] :

IsOpen (exterior s)

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

exterior s ∈ nhdsSet s

@[simp]

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

exterior s = s ↔ IsOpen s

@[simp]

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

exterior s ⊆ s ↔ IsOpen s

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

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

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

exterior s ⊆ t ↔ t ∈ nhdsSet s

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

exterior {a} ⊆ t ↔ t ∈ nhds a

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

exterior s ⊆ t ↔ s ⊆ t

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

GaloisConnection exterior interior

@[simp]

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

exterior (exterior s) = exterior s

@[simp]

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

exterior (s ∪ t) = exterior s ∪ exterior t

@[simp]

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

nhdsSet (exterior s) = nhdsSet s

@[simp]

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

Filter.principal (exterior s) = nhdsSet s

@[simp]

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

exterior s ⊆ exterior t ↔ nhdsSet s ≤ nhdsSet t

theorem specializes_iff_exterior_subset {α : Type u_3} [TopologicalSpace α] {x : α} {y : α} [AlexandrovDiscrete α] :

x ⤳ y ↔ exterior {x} ⊆ exterior {y}

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

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

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

IsCompact (exterior s)

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

AlexandrovDiscrete β

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

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 α

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

FirstCountableTopology α

Equations

(_ : FirstCountableTopology α) = (_ : FirstCountableTopology α)

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

LocallyCompactSpace α

Equations

(_ : LocallyCompactSpace α) = (_ : LocallyCompactSpace α)

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

AlexandrovDiscrete { a : α // p a }

Equations

(_ : AlexandrovDiscrete { a : α // p a }) = (_ : AlexandrovDiscrete { x : α // x ∈ fun (a : α) => p a })

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

AlexandrovDiscrete (Quotient s)

Equations

(_ : AlexandrovDiscrete (Quotient s)) = (_ : AlexandrovDiscrete (Quotient s))

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

AlexandrovDiscrete (α ⊕ β)

Equations

(_ : AlexandrovDiscrete (α ⊕ β)) = (_ : AlexandrovDiscrete (α ⊕ β))

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

AlexandrovDiscrete ((i : ι) × π i)

Equations

(_ : AlexandrovDiscrete ((i : ι) × π i)) = (_ : AlexandrovDiscrete ((i : ι) × π i))