This file contains additional definitions and statements around covers of topological spaces which are useful for properties and theorems.

def PiBase.PointFiniteAt {X : Type u_1} {ι : Type u_2} (U : ι → Set X) (x : X) : Prop

A collection of sets is called point finite at a point x if it meets x only finitely many times.

Equations

• PiBase.PointFiniteAt U x = {i : ι | x ∈ U i}.Finite

def PiBase.PointFinite {X : Type u_1} {ι : Type u_2} (U : ι → Set X) : Prop

A collection of sets is called point finite if it is point finite at each point.

Equations

• PiBase.PointFinite U = ∀ (x : X), {i : ι | x ∈ U i}.Finite

def PiBase.PointCountable {X : Type u_1} {ι : Type u_2} (U : ι → Set X) : Prop

A collection of sets is called point countable if it meets every point only countably many times.

Equations

• PiBase.PointCountable U = ∀ (x : X), {i : ι | x ∈ U i}.Countable

def PiBase.CoverStar {X : Type u_1} {ι : Type u_2} (U : ι → Set X) (x : X) : Set X

Star of an open cover.

Equations

• PiBase.CoverStar U x = ⋃ (i : ι), ⋃ (_ : x ∈ U i), U i

def PiBase.StarFinite {X : Type u_1} {ι : Type u_2} (U : ι → Set X) : Prop

A collection of sets is called star finite if each member of the collection only meets finitely many other member.

Equations

• PiBase.StarFinite U = ∀ (i : ι), {j : ι | (U j ∩ U i).Nonempty}.Finite

theorem PiBase.PointFinite.pointCountable {X : Type u_1} {ι : Type u_2} {U : ι → Set X} (h : PointFinite U) : PointCountable U

A point finite collection of sets is point countable.

theorem PiBase.Finite.starFinite {X : Type u_1} {ι : Type u_2} (U : ι → Set X) (h : Finite ι) : StarFinite U

A finite family of sets is star finite.

theorem PiBase.Finite.locallyFinite {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (U : ι → Set X) (h : Finite ι) : LocallyFinite U

A finite family of sets is locally finite.

theorem PiBase.StarFinite.PointFinite {X : Type u_1} {ι : Type u_2} {U : ι → Set X} (h : StarFinite U) : PiBase.PointFinite U

A star finite collection of sets is point finite.

def PiBase.LocallyCountable {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (U : ι → Set X) : Prop

A family of sets in Set X is locally finite if at every point x : X, there is a neighborhood of x which meets only countably many sets in the family.

Equations

• PiBase.LocallyCountable U = ∀ (x : X), ∃ t ∈ nhds x, {i : ι | (U i ∩ t).Nonempty}.Countable

theorem PiBase.Countable.locallyCountable {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (U : ι → Set X) (h : Countable ι) : LocallyCountable U

A countable family of sets is locally countable.

theorem PiBase.LocallyFinite.locallyCountable {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {U : ι → Set X} (h : LocallyFinite U) : LocallyCountable U

A locally finite collection of sets is locally countable.

def PiBase.IsDiscreteFamily {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (F : ι → Set X) : Prop

A discrete family of sets.

Equations

• PiBase.IsDiscreteFamily F = ∀ (x : X), ∃ U ∈ nhds x, {i : ι | (F i ∩ U).Nonempty}.Subsingleton

def PiBase.IsOmegaCover {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (f : ι → TopologicalSpace.Opens X) : Prop

An omega cover of a space.

Equations

• PiBase.IsOmegaCover f = (TopologicalSpace.IsOpenCover f ∧ ⊤ ∉ Set.range f ∧ ∀ (s : Finset X), ∃ (i : ι), ↑s ⊆ ↑(f i))

theorem PiBase.LocallyFinite.PointFinite {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {U : ι → Set X} (h : LocallyFinite U) : PiBase.PointFinite U

A locally finite collection of sets is point finite.

theorem PiBase.StarFinite.locallyFinite {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {U : ι → Set X} (h : StarFinite U) (U_open : ∀ (a : ι), IsOpen (U a)) (U_cover : ⋃ (a : ι), U a = Set.univ) : LocallyFinite U

A star finite open cover is locally finite.

theorem Set.Countable.diff {α : Type u} {s t : Set α} (hs : s.Countable) : (s \ t).Countable

theorem PiBase.LocallyCountable.pointCountable {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {U : ι → Set X} (h : LocallyCountable U) : PointCountable U

A locally countable collection of sets is point countable.

def PiBase.IsNetwork {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (f : ι → Set X) : Prop

A network of a topological space.

Equations

• PiBase.IsNetwork f = ∀ (x : X), ∀ s ∈ nhds x, ∃ (i : ι), x ∈ f i ∧ f i ⊆ s

def PiBase.IsKNetwork {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (f : ι → Set X) : Prop

A k-network of a topological space.

Equations

• PiBase.IsKNetwork f = ∀ (U K : Set X), IsOpen U → IsCompact K → K ⊆ U → ∃ (s : Finset ι), K ⊆ ⋃ i ∈ s, f i ∧ ⋃ i ∈ s, f i ⊆ U

theorem PiBase.IsKNetwork.isNetwork {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {f : ι → Set X} (h : IsKNetwork f) : IsNetwork f

Every k-network is a network

def PiBase.IsKCover {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (f : ι → TopologicalSpace.Opens X) : Prop

K-cover of a topological space

Equations

• PiBase.IsKCover f = (TopologicalSpace.IsOpenCover f ∧ ⊤ ∉ Set.range f ∧ ∀ ⦃K : Set X⦄, IsCompact K → ∃ (i : ι), K ⊆ ↑(f i))

def PiBase.IsKCover' {X : Type u_1} [TopologicalSpace X] (s : Set (Set X)) : Prop

Alternative def of K covers

Equations

• PiBase.IsKCover' s = ((∀ i ∈ s, IsOpen i) ∧ ⋃₀ s = Set.univ ∧ Set.univ ∉ s ∧ ∀ ⦃K : Set X⦄, IsCompact K → ∃ i ∈ s, K ⊆ i)

def PiBase.IsKCover'' {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (f : ι → Set X) : Prop

K-cover of a topological space

Equations

• PiBase.IsKCover'' f = ((∀ (i : ι), IsOpen (f i)) ∧ ⋃ (i : ι), f i = Set.univ ∧ Set.univ ∉ Set.range f ∧ ∀ ⦃K : Set X⦄, IsCompact K → ∃ (i : ι), K ⊆ f i)