coe_prodCongr — Mathlib

English

The underlying function of the product congruence is the product of the underlying functions.

Русский

Осуществление подлежащей функции произведения конгруэнтности равно произведению функций-оснований.

LaTeX

$$$\\forall {\\alpha \\beta} {\\gamma \\delta} [UniformSpace \\alpha] [UniformSpace \\beta] [UniformSpace \\gamma] [UniformSpace \\delta],\\; (h_1.prodCongr h_2)^{-1} = Prod.map h_1 h_2$$$

Lean4

@[simp]
theorem coe_prodCongr (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂ :=
  rfl

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