modelWithCorners_prod_coe — Mathlib

English

The product construction commutes with the model-with-corners coe: the forward projection matches the product map.

Русский

Произведение конструкций совместимо с отображением модели с углами: отображение в произведение совпадает с произведением отображений.

LaTeX

$$ (I.prod J).toPartialEquiv = I.toPartialEquiv.prod J.toPartialEquiv $$

Lean4

@[simp, mfld_simps]
theorem modelWithCorners_prod_coe (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') :
    (I.prod I' : _ × _ → _ × _) = Prod.map I I' :=
  rfl

Похожие утверждения