English
For a finite family of model-with-corners I_i, there is a product model with corners on the product of E_i with ModelPi H, i.e. the functor I_i produces a product model.
Русский
Для конечной семейства I_i имеется произведение моделей с углами на произведении пространств E_i с моделью ModelPi H.
LaTeX
$$$$ \text{ModelWithCorners } \pi(I_i) \;:\; \text{ModelWithCorners } \prod_i E_i \; (\text{ModelPi } H). $$$$
Lean4
/-- Given a finite family of `ModelWithCorners` `I i` on `(E i, H i)`, we define the model with
corners `pi I` on `(Π i, E i, ModelPi H)`. See note [Manifold type tags] for explanation about
`ModelPi H`. -/
def pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Type v} [Fintype ι] {E : ι → Type w}
[∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] {H : ι → Type u'} [∀ i, TopologicalSpace (H i)]
(I : ∀ i, ModelWithCorners 𝕜 (E i) (H i)) : ModelWithCorners 𝕜 (∀ i, E i) (ModelPi H)
where
toPartialEquiv := PartialEquiv.pi fun i => (I i).toPartialEquiv
source_eq := by simp only [pi_univ, mfld_simps]
convex_range' := by
rw [PartialEquiv.pi_apply, Set.range_piMap]
split_ifs with h
· letI := h.rclike
letI := fun i ↦ NormedSpace.restrictScalars ℝ 𝕜 (E i)
exact convex_pi fun i _hi ↦ (I i).convex_range
· simp [range_eq_univ_of_not_isRCLikeNormedField, h]
nonempty_interior' := by
rw [PartialEquiv.pi_apply, Set.range_piMap]
simp [interior_pi_set finite_univ, univ_pi_nonempty_iff, nonempty_interior]
continuous_toFun := continuous_pi fun i => (I i).continuous.comp (continuous_apply i)
continuous_invFun := continuous_pi fun i => (I i).continuous_symm.comp (continuous_apply i)
