instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem

English

If G acts by scalar multiplication on each R_i and the action is continuous on each factor, then the restricted product inherits a continuous action.

Русский

Если G действует скалярно на каждом R_i и действие непрерывно на каждом факторе, то ограниченное произведение наследует непрерывное действие.

LaTeX

$$$\\mathrm{ContinuousSmul}\\left(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{B_i\\}; \\mathrm{cofinite})\\right)$$$

Lean4

@[to_additive]
instance [Π i, Group (R i)] [∀ i, SubgroupClass (S i) (R i)] [∀ i, IsTopologicalGroup (R i)]
    [hAcompact : ∀ i, CompactSpace (B i)] : LocallyCompactSpace (Πʳ i, [R i, B i]) :=
  -- TODO: extract as a lemma

  haveI : ∀ i, WeaklyLocallyCompactSpace (R i) := fun i ↦
    .mk fun x ↦
      ⟨x • (B i : Set (R i)), .smul _ (isCompact_iff_compactSpace.mpr inferInstance),
        hBopen.out i |>.smul _ |>.mem_nhds <| by simpa using smul_mem_smul_set (a := x) (one_mem (B i))⟩
  locallyCompactSpace_of_group _ <| .of_forall fun _ ↦ isCompact_iff_compactSpace.mpr inferInstance

Похожие утверждения