instIsTopologicalAddTorsorProd — Mathlib

English

For a family of topological additive torsors (V_i, P_i) over an index set i, the product (V_i) → (P_i) forms a topological additive torsor under the product group, with coordinatewise action and product topology.

Русский

Для семейства топологических аддитивных торсоров (V_i, P_i) по индексу i образуется торсор под действием произведения, с действиями по координатам и топологией произведения.

LaTeX

$$$IsTopologicalAddTorsor\\bigl(\\prod_i P_i\\bigr) \\text{ under } (\\prod_i V_i) \\text{ with } (v_i)\\cdot(p_i)=(v_i+ᵥ p_i)_i.$$$

Lean4

instance : IsTopologicalAddTorsor (P × Q)
    where
  continuous_vadd := Continuous.prodMk (by fun_prop) (by fun_prop)
  continuous_vsub := Continuous.prodMk (by fun_prop) (by fun_prop)

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