English
The product of two C^n manifolds is again a C^n manifold, compatibly with the product model I.prod I'.
Русский
Произведение двух C^n-многообразий образует снова C^n-многообразие, конфигурированное через произведение моделей I.prod I'.
LaTeX
$$IsManifold I n M ∧ IsManifold I' n M' ⇒ IsManifold (I.prod I') n (M × M')$$
Lean4
/-- The product of two `C^n` manifolds is naturally a `C^n` manifold. -/
instance prod {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type*}
[NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (M : Type*) [TopologicalSpace M]
[ChartedSpace H M] [IsManifold I n M] (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' n M'] :
IsManifold (I.prod I') n (M × M') where
compatible := by
rintro f g ⟨f1, hf1, f2, hf2, rfl⟩ ⟨g1, hg1, g2, hg2, rfl⟩
rw [OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.prod_trans]
have h1 := (contDiffGroupoid n I).compatible hf1 hg1
have h2 := (contDiffGroupoid n I').compatible hf2 hg2
exact contDiffGroupoid_prod h1 h2
