Theorems · Theorem · Lie groups

RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite

∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ [∀ (i : ι), WeaklyLocallyCompactSpace (R i)],
      (∀ᶠ (i : ι) in Filter.cofinite, IsCompact (A i)) →
        WeaklyLocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite)

If each R i is weakly locally compact, each A i is open, and all but finitely many A is are also compact, then the restricted product Πʳ i, [R i, A i] is weakly locally compact.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceWeaklyLocallyCompactSpace