prodCongr_symm — Mathlib

English

The inverse of the product congruence equals the product of the inverses.

Русский

Обратное к произведению конгруэнтности равно произведению обратных конгруэнтностей.

LaTeX

$$$\\forall {\\alpha \\beta \\gamma \\delta} [UniformSpace \\alpha] [UniformSpace \\beta] [UniformSpace \\gamma] [UniformSpace \\delta],\\; (h_1.prodCongr h_2).\\text{symm} = h_1.symm.prodCongr h_2.symm$$$

Lean4

@[simp]
theorem prodCongr_symm (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm :=
  rfl

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