Theorems · Theorem · Lie groups

RestrictedProduct.weaklyLocallyCompactSpace_of_principal

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

Assume that S is a subset of ι with finite complement, that each R i is weakly locally compact, and that A i is compact for all i ∈ S. Then the restricted product Πʳ i, [R i, A i]_[𝓟 S] is locally compact. Note: we spell "S has finite complement" as cofinite ≤ 𝓟 S.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceWeaklyLocallyCompactSpace