prod_coe — Mathlib

English

The underlying map of the product is the product of the underlying maps.

Русский

Функция, лежащая в основе произведения, есть параллельная функциям-основам каждого компонента.

LaTeX

$$$ (e.prod e').toFun p = (e.toFun p.1, e'.toFun p.2) $$$

Lean4

@[simp, mfld_simps]
theorem prod_coe (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    (e.prod e' : α × γ → β × δ) = fun p => (e p.1, e' p.2) :=
  rfl

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