isIso_arrow_iff_eq_top

Mathlib.CategoryTheory.Subobject.Lattice

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

English

For a subobject P of Y, P.arrow is iso iff P = ⊤.

Русский

Стрела P.arrow из подпредмета P в Y изоморфна тогда и только тогда, когда P = ⊤.

LaTeX

$$$\text{IsIso } P.\text{arrow} \iff P = \top$$$

Lean4

theorem isIso_arrow_iff_eq_top {Y : C} (P : Subobject Y) : IsIso P.arrow ↔ P = ⊤ := by
  rw [isIso_iff_mk_eq_top, mk_arrow]

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

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

Разделы

Аффилиация

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