continuousMul_of_contMDiffMul — Mathlib

English

The product map is ContMDiff; i.e., the map (u,v) ↦ u v from G × G to G is C^n.

Русский

Карта умножения на произведение является ContMDiff, т.е. (u,v) ↦ uv из G×G в G — C^n.

LaTeX

$$$$ \ContMDiff (I \prod I) I n \bigl(\lambda p : G \times G, p_1 p_2\bigr) $$$$

Lean4

/-- If the multiplication is `C^n`, then it is continuous. This is not an instance for technical
reasons, see note [Design choices about smooth algebraic structures]. -/
@[to_additive /-- If the addition is `C^n`, then it is continuous. This is not an instance for
    technical reasons, see note [Design choices about smooth algebraic structures]. -/
    ]
theorem continuousMul_of_contMDiffMul [ContMDiffMul I n G] : ContinuousMul G :=
  ⟨(contMDiff_mul I n).continuous⟩

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