inverts

Mathlib.CategoryTheory.Localization.Predicate

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

English

W is inverted by L: every W-morphism becomes isomorphism after localization.

Русский

W-инвертируется локализацией: каждый морфизм W становится изоморфизмом после локализации.

LaTeX

$$$W.IsInvertedBy L$$$

Lean4

theorem inverts : W.IsInvertedBy L :=
  (inferInstance : L.IsLocalization W).inverts

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

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

Разделы

Аффилиация

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