Networks and monolithic spaces

DefinitionCountable network#✓fully proved

A topological space \(X\) has a countable network if there is a countable family \(\mathcal{N}\) of subsets of \(X\) such that for every open set \(U \subseteq X\) and every point \(x \in U\) there is some \(V \in \mathcal{N}\) with \(x \in V \subseteq U\).

Network sets need not themselves be open.

def HasCountableNetwork (X : Type*) [TopologicalSpace X] : Prop :=
  ∃ 𝒩 : Set (Set X), 𝒩.Countable ∧
    ∀ ⦃U : Set X⦄, IsOpen U → ∀ x ∈ U,
      ∃ V ∈ 𝒩, x ∈ V ∧ V ⊆ U

Used by 2

Used byCountably monolithic space · Second-countable spaces have a countable network

TheoremSecond-countable spaces have a countable network#✓fully proved

Every second-countable topological space has a countable network.

theorem hasCountableNetwork_of_secondCountable (X : Type*) [TopologicalSpace X]
    [SecondCountableTopology X] : HasCountableNetwork X

Uses 1

Statement usesCountable network

ClassCountably monolithic space#✓fully proved

A topological space is countably monolithic (ω-monolithic) if the closure of every countable subspace has a countable network.

class CountablyMonolithicSpace (X : Type*) [TopologicalSpace X] : Prop where
  hasCountableNetwork_closure_of_countable :
    ∀ ⦃s : Set X⦄, s.Countable → HasCountableNetwork ↥(closure s)

Uses 1

Statement usesCountable network

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.