Structures · Topology

ParacompactSpace

A topological space is called paracompact, if every open covering of this space admits a locally finite refinement. We use the same universe for all types in the definition to avoid creating a class like ParacompactSpace.{u v}. Due to lemma precise_refinement below, every open covering s : α → Set X indexed on α : Type v has a precise locally finite refinement, i.e., a locally finite refinement t : α → Set X indexed on the same type such that each ∀ i, t i ⊆ s i.

Defined in

Mathlib.Topology.Compactness.Paracompact

Shape

One type argument · adds locallyFinite_refinement