ofBialgHom_symm — Mathlib

English

The inverse of the constructed equivalence equals the constructed with swapped data: (ofBialgHom f g h1 h2)^{-1} = ofBialgHom g f h2 h1.

Русский

Обратное к построенной эквивалентности равно эквивалентности, полученной из swapped-данных: (ofBialgHom f g h1 h2)^{-1} = ofBialgHom g f h2 h1.

LaTeX

$$$\\left(\\operatorname{ofBialgHom}(f,g,h_1,h_2)\\right)^{-1} = \\operatorname{ofBialgHom}(g,f,h_2,h_1)$$$

Lean4

theorem ofBialgHom_symm (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ h₂) :
    (ofBialgHom f g h₁ h₂).symm = ofBialgHom g f h₂ h₁ :=
  rfl

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