Theorems · Theorem · general topology

ParacompactSpace.locallyFinite_refinement

∀ {X : Type v} {inst : TopologicalSpace X} [self : ParacompactSpace X] (α : Type v) (s : α → Set X),
  (∀ (a : α), IsOpen (s a)) →
    ⋃ a, s a = Set.univ →
      ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Every open cover of a paracompact space assumes a locally finite refinement.

Defined in

Mathlib.Topology.Compactness.Paracompact

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

ParacompactSpace