symm_mk — Mathlib

English

The symm of a constructed star ring equivalence corresponds to swapping the forward and inverse components.

Русский

Обратное отображение симметрически конструированного эквивалентного звёздного кольца соответствует обмену компонентами.

LaTeX

$$$\\big( \\langle \\langle \\langle f,f',h_1,h_2\\rangle,h_3,h_4\\rangle,h_5\\rangle : A \\simeq_{\\star} B \\big).\\mathrm{symm} = \\{\\text{...swap ...}\\}$$$

Lean4

@[simp]
theorem symm_mk (f f') (h₁ h₂ h₃ h₄ h₅) :
    (⟨⟨⟨f, f', h₁, h₂⟩, h₃, h₄⟩, h₅⟩ : A ≃⋆+* B).symm =
      { symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ with
        toFun := f'
        invFun := f } :=
  rfl

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