wInv

Mathlib.CategoryTheory.Localization.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.Construction.wInv

Lean4

/-- The formal inverse in `W.Localization` of a morphism `w` in `W`. -/
abbrev wInv {X Y : C} (w : X ⟶ Y) (hw : W w) :=
  (wIso w hw).inv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru