inv_mk — Mathlib

English

The equality of inverses in the AEEqFun structure reflects the underlying construction.

Русский

Равенство обратных элементов в структуре AEEqFun отражает основную конструкцию.

LaTeX

$$$\text{Eq}\ (\mathrm{instInv.inv} (\mathrm{mk} f hf)) = \mathrm{mk} (f^{-1}) (hf.inv)$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_mk (f : α → γ) (hf) : (mk f hf : α →ₘ[μ] γ)⁻¹ = mk f⁻¹ hf.inv :=
  rfl

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