English
Given two model-with-corners I on (E,H) and J on (E',H'), their product I.prod J is a model-with-corners on (E×E') with modelProd H H'.
Русский
Заданы две модели с гранями I на (E,H) и J на (E',H'); их произведение I.prod J является моделью с углами на (E×E') с моделью-modelProd H H'.
LaTeX
$$$$ (I \text{ .prod } J): \text{ModelWithCorners } 𝕜 (E \times E') (\text{ModelProd } H H'). $$$$
Lean4
/-- Given two model_with_corners `I` on `(E, H)` and `I'` on `(E', H')`, we define the model with
corners `I.prod I'` on `(E × E', ModelProd H H')`. This appears in particular for the manifold
structure on the tangent bundle to a manifold modelled on `(E, H)`: it will be modelled on
`(E × E, H × E)`. See note [Manifold type tags] for explanation about `ModelProd H H'`
vs `H × H'`. -/
@[simps -isSimp]
def prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w}
[TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
{H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') :
ModelWithCorners 𝕜 (E × E') (ModelProd H H') :=
{
I.toPartialEquiv.prod I'.toPartialEquiv with
toFun := fun x => (I x.1, I' x.2)
invFun := fun x => (I.symm x.1, I'.symm x.2)
source := {x | x.1 ∈ I.source ∧ x.2 ∈ I'.source}
source_eq := by simp only [setOf_true, mfld_simps]
convex_range' :=
by
have : range (fun (x : ModelProd H H') ↦ (I x.1, I' x.2)) = range (Prod.map I I') := rfl
rw [this, Set.range_prodMap]
split_ifs with h
· letI := h.rclike
letI := NormedSpace.restrictScalars ℝ 𝕜 E; letI := NormedSpace.restrictScalars ℝ 𝕜 E'
exact I.convex_range.prod I'.convex_range
· simp [range_eq_univ_of_not_isRCLikeNormedField, h]
nonempty_interior' :=
by
have : range (fun (x : ModelProd H H') ↦ (I x.1, I' x.2)) = range (Prod.map I I') := rfl
simp [this, interior_prod_eq, nonempty_interior]
continuous_toFun := I.continuous_toFun.prodMap I'.continuous_toFun
continuous_invFun := I.continuous_invFun.prodMap I'.continuous_invFun }
