English
If M and N are analytic manifolds, then their product M × N is an analytic manifold.
Русский
Если M и N являются аналитическими многообразиями, то их произведение M × N тоже является аналитическим многообразием.
LaTeX
$$$\text{AnalyticManifold}(I,J) \; \Rightarrow \; \text{AnalyticManifold}(I \prod J)\, (M \times N)$$$
Lean4
/-- `M × N` is an analytic manifold if `M` and `N` are -/
instance prod {E A : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace A] {F B : Type}
[NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {I : ModelWithCorners 𝕜 E A}
{J : ModelWithCorners 𝕜 F B} {M : Type} [TopologicalSpace M] [ChartedSpace A M] [m : AnalyticManifold I M]
{N : Type} [TopologicalSpace N] [ChartedSpace B N] [n : AnalyticManifold J N] : AnalyticManifold (I.prod J) (M × N)
where
compatible := by
intro f g ⟨f1, f2, hf1, hf2, fe⟩ ⟨g1, g2, hg1, hg2, ge⟩
rw [← fe, ← ge, OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.prod_trans]
exact analyticGroupoid_prod (m.toHasGroupoid.compatible f2 g2) (n.toHasGroupoid.compatible hf2 hg2)
