continuous_mul' — Mathlib

English

The map (x,y) ↦ x*y is continuous on the product space.

Русский

Отображение $(x,y) \\mapsto x y$ непрерывно на произведении пространств.

LaTeX

$$$\\text{Continuous}\\bigl(p \\mapsto p_1 \\cdot p_2\\bigr)$ where $p\\in \\alpha \\times \\alpha$$$

Lean4

/-- A version of the global `continuous_mul` suitable for dot notation. -/
@[to_additive /-- A version of the global `continuous_add` suitable for dot notation. -/
    ]
theorem continuous_mul' (g : GroupTopology α) :
    haveI := g.toTopologicalSpace
    Continuous fun p : α × α => p.1 * p.2 :=
  by
  letI := g.toTopologicalSpace
  haveI := g.toIsTopologicalGroup
  exact continuous_mul

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