Theorems · Theorem · Lie groups

RestrictedProduct.locallyCompactSpace_of_group

∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)]
  [∀ (i : ι), LocallyCompactSpace (R i)],
  (∀ᶠ (i : ι) in Filter.cofinite, IsCompact ↑(B i)) →
    LocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)

Assume that each R i is a locally compact group with A i an open subgroup. Assume also that all but finitely many A is are compact. Then the restricted product Πʳ i, [R i, A i] is a locally compact group.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

SetLikeTopologicalSpaceFactGroupSubgroupClassIsTopologicalGroupLocallyCompactSpace