instIsTopologicalAddTorsorForall — Mathlib

English

The family of topological additive torsors indexed by i has a product structure: the product is a topological additive torsor with the product action and product topology.

Русский

Семейство топологических аддитивных торсоров с индексами образует произведение, которое является топологическим аддитивным торсором с произведением действия и топологией.

LaTeX

$$$IsTopologicalAddTorsor\\Big( (i\\mapsto P_i) \\Big) \\text{ under } (i\\mapsto V_i), \\text{ with product action and topology }$$$

Lean4

instance : IsTopologicalAddTorsor ((i : ι) → P i)
    where
  continuous_vadd := continuous_pi <| by simp only [Pi.vadd_apply']; fun_prop
  continuous_vsub := continuous_pi <| by simp only [Pi.vsub_apply]; fun_prop

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