prop_isoClosure — Mathlib

English

Let P be a property of objects in a category C. If X has P and Y is isomorphic to X, then Y lies in the iso-closure of P.

Русский

Пусть P — свойство объектов в категории C. Если у X есть свойство P и Y изоморф с X, тогда Y принадлежит изоморфному замыканию P.

LaTeX

$$$$ P(X) \land X \cong Y \Rightarrow isoClosure(P)(Y). $$$$

Lean4

theorem prop_isoClosure {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : isoClosure P Y :=
  ⟨X, h, ⟨(asIso e).symm⟩⟩

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