prop_iff_of_isIso

Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.prop_iff_of_isIso

English

For P closed under isomorphisms, and any isomorphism f : X ≅ Y, P X ↔ P Y.

Русский

Для P замкнутого по изоморфизмам и любой изоморфизм f : X ≅ Y верно P X ⇔ P Y.

LaTeX

$$$ P X \leftrightarrow P Y $ при e : X \cong Y$$

Lean4

theorem prop_iff_of_isIso [IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y :=
  prop_iff_of_iso P (asIso f)

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

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

Разделы

Аффилиация

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