instIsClosedUnderIsomorphismsIsoClosure

English

If P is closed under isomorphisms, then isoClosure(P) is also closed under isomorphisms.

Русский

Если P замкнуто по изоморфизмам, то и isoClosure(P) замкнуто по изоморфизмам.

LaTeX

$$$$ [P.IsClosedUnderIsomorphisms] \Rightarrow isoClosure(P).IsClosedUnderIsomorphisms. $$$$

Lean4

instance : IsClosedUnderIsomorphisms (isoClosure P) where
  of_iso := by
    rintro X Y e ⟨Z, hZ, ⟨f⟩⟩
    exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩

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