English
Let ι be a finite index set. If for every i ∈ ι we have a charted space (M_i, H_i) with each H_i a topological space, then the finite product space ModelPi H = ∏_{i∈ι} M_i carries a natural charted-space structure. Its atlas is obtained by taking the product of the factor atlases via the canonical projection maps, i.e., the charts are the coordinatewise product of the charts from each factor.
Русский
Пусть имеется конечное множество индексов ι. Пусть для каждого i ∈ ι задано чартизированное пространство (M_i, H_i) с соответствующим топологическим пространством H_i. Тогда конечный произведение M = ∏_{i∈ι} M_i естественно оборудуется структурой чартизованного пространства. Атлас этого пространства получается как произведение атласов компонент, через канонические проекции, т.е.Charts — это координатно-образующие карты, полученные по произведению карт каждого множества.
LaTeX
$$$\text{ChartedSpace}(\mathrm{ModelPi}\, H, \forall i, M_i)\;\text{with}\\\n\operatorname{atlas}(\mathrm{ModelPi}\, H) = \operatorname{OpenPartialHomeomorph.pi}''\big(\mathrm{Set.pi}\,\mathrm{univ} \; (\lambda i \mapsto \operatorname{atlas}(H_i)(M_i))\big).$$$
Lean4
/-- The product of a finite family of charted spaces is naturally a charted space, with the
canonical construction of the atlas of finite product maps. -/
instance piChartedSpace {ι : Type*} [Finite ι] (H : ι → Type*) [∀ i, TopologicalSpace (H i)] (M : ι → Type*)
[∀ i, TopologicalSpace (M i)] [∀ i, ChartedSpace (H i) (M i)] : ChartedSpace (ModelPi H) (∀ i, M i)
where
atlas := OpenPartialHomeomorph.pi '' Set.pi univ fun _ ↦ atlas (H _) (M _)
chartAt f := OpenPartialHomeomorph.pi fun i ↦ chartAt (H i) (f i)
mem_chart_source f i _ := mem_chart_source (H i) (f i)
chart_mem_atlas f := mem_image_of_mem _ fun i _ ↦ chart_mem_atlas (H i) (f i)
