wInv_eq_isoOfHom_inv — Mathlib

English

The wInv construction equals the inverse of isoOfHom in the appropriate localization setting.

Русский

Конструкция wInv равна обратному изоморфизму в соответствующей локализационной настройке.

LaTeX

$$$wInv f hf = (isoOfHom W.Q W f hf)^{-1}$$$

Lean4

theorem wInv_eq_isoOfHom_inv {X Y : C} (f : X ⟶ Y) (hf : W f) : Construction.wInv f hf = (isoOfHom W.Q W f hf).inv :=
  congr_arg Iso.inv (wIso_eq_isoOfHom f hf)

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