symm_mk — Mathlib

English

The inverse of a constructed ring isomorphism mk is the isomorphism with toFun and invFun swapped.

Русский

Обратная сущность построенного изоморфизма mk есть изоморфизм, в котором функции-образ и обратная функции поменяны местами.

LaTeX

$$$\\left( \\mathrm{mk} \\langle f,g,h_1,h_2 \\rangle h_3 h_4 \\right)^{-1} = \\{\\text{symm\_mk.aux } f g h_1 h_2 h_3 h_4 \\text{ with } toFun = g, invFun = f\\}$$$

Lean4

@[simp]
theorem symm_mk (f : R → S) (g h₁ h₂ h₃ h₄) :
    (mk ⟨f, g, h₁, h₂⟩ h₃ h₄).symm =
      { symm_mk.aux f g h₁ h₂ h₃ h₄ with
        toFun := g
        invFun := f } :=
  rfl

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