Theorems · Definition · general topology

LocallyFinite.encodable

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    [SigmaCompactSpace X] →
      {ι : Type u_4} → {f : ι → Set X} → LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Encodable ι

If f : ι → Set X is a locally finite covering of a σ-compact topological space by nonempty sets, then the index type ι is encodable.

Defined in

Mathlib.Topology.Compactness.SigmaCompact

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceSigmaCompactSpace