nhds_zero_eq_map_structureMap — Mathlib

English

If a group G acts on each R_i by scalar multiplication with compatible subobjects B_i, then the diagonal action on the restricted product is continuous.

Русский

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

LaTeX

$$$\\mathrm{ContinuousSmul}\\big(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{B_i\\}; \\mathrm{principal}(T))\\big)$$$

Lean4

theorem nhds_zero_eq_map_structureMap [Π i, Zero (R i)] [∀ i, ZeroMemClass (S i) (R i)]
    (hBopen : ∀ i, IsOpen (B i : Set (R i))) :
    (𝓝 (structureMap R (fun i ↦ B i) cofinite 0)) = .map (structureMap R (fun i ↦ B i) cofinite) (𝓝 0) :=
  nhds_eq_map_structureMap hBopen
    0
      -- TODO: Make `IsOpen` a class like `IsClosed` ?

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