English
There is a canonical ContMDiffMul structure on the product G × G' given by the product of structures on G and G'.
Русский
Пространство произведения G × G' может быть снабжено канонической структурой ContMDiffMul, полученной по произведению структур на G и G'.
LaTeX
$$ContMDiffMul (I.prod I') n (G × G')$$
Lean4
@[to_additive prod]
instance prod {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
[TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (G : Type*) [TopologicalSpace G] [ChartedSpace H G] [Mul G]
[ContMDiffMul I n G] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H') (G' : Type*) [TopologicalSpace G'] [ChartedSpace H' G'] [Mul G']
[ContMDiffMul I' n G'] : ContMDiffMul (I.prod I') n (G × G') :=
{ IsManifold.prod G G' with
contMDiff_mul :=
((contMDiff_fst.comp contMDiff_fst).mul (contMDiff_fst.comp contMDiff_snd)).prodMk
((contMDiff_snd.comp contMDiff_fst).mul (contMDiff_snd.comp contMDiff_snd)) }
