English
If two model with corners I and I' are boundaryless, then their product is boundaryless.
Русский
Если два модели с углами без границы, их произведение тоже без границы.
LaTeX
$$$ (I.\text{prod} I').\text{Boundaryless}$$$
Lean4
/-- If two model with corners are boundaryless, their product also is -/
instance range_eq_univ_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E]
[NormedSpace 𝕜 E] {H : Type w} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] {E' : Type v'}
[NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
[I'.Boundaryless] : (I.prod I').Boundaryless := by
constructor
dsimp [ModelWithCorners.prod, ModelProd]
rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ, ModelWithCorners.Boundaryless.range_eq_univ,
univ_prod_univ]
