English
For a finite family (H_i, M_i) of charted spaces and a tuple f = (f_i) with f_i ∈ M_i, the chart at f in the product space ModelPi H is exactly the product of the component charts: chartAt(H)(f) = OpenPartialHomeomorph.pi( chartAt(H_i)(f_i) )_i.
Русский
Для конечной семьи чартизированных пространств (H_i, M_i) и кортежа f = (f_i) с f_i ∈ M_i, картa на точке f в произведении равна произведению компонентных карт: chartAt(H)(f) = OpenPartialHomeomorph.pi( chartAt(H_i)(f_i) )_i.
LaTeX
$$$chartAt(H)(f) = OpenPartialHomeomorph.pi\big( i \mapsto chartAt(H_i)(f_i) \big).$$$
Lean4
@[simp, mfld_simps]
theorem piChartedSpace_chartAt {ι : Type*} [Finite ι] (H : ι → Type*) [∀ i, TopologicalSpace (H i)] (M : ι → Type*)
[∀ i, TopologicalSpace (M i)] [∀ i, ChartedSpace (H i) (M i)] (f : ∀ i, M i) :
chartAt (H := ModelPi H) f = OpenPartialHomeomorph.pi fun i ↦ chartAt (H i) (f i) :=
rfl
