modelWithCorners_prod_toPartialEquiv

English

Product of model-with-corners respects the projections: the toPartialEquiv of the product equals the product of the toPartialEquivs.

Русский

Произведение моделей с углами сохраняет проекции: toPartialEquiv произведения равно произведению toPartialEquivs.

LaTeX

$$$$ (I \text{ prod } J).toPartialEquiv = I.toPartialEquiv .prod J.toPartialEquiv. $$$$

Lean4

@[simp, mfld_simps]
theorem modelWithCorners_prod_toPartialEquiv : (I.prod J).toPartialEquiv = I.toPartialEquiv.prod J.toPartialEquiv :=
  rfl

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