eq_top_of_isIso_arrow

Mathlib.CategoryTheory.Subobject.Lattice

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.eq_top_of_isIso_arrow

English

Reiterates that if the arrow of a subobject is an isomorphism, then the subobject is top.

Русский

Повтор: если стрелка подпредмета изоморфна, то подпредмет равен верхнему.

LaTeX

$$$\text{If } P.\text{arrow is iso, then } P = \top$$$

Lean4

theorem eq_top_of_isIso_arrow {Y : C} (P : Subobject Y) [IsIso P.arrow] : P = ⊤ :=
  (isIso_arrow_iff_eq_top P).mp inferInstance

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

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

Разделы

Аффилиация

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