corepresentable_of_natIso — Mathlib

English

Corepresentability is preserved under a natural isomorphism: if F ≅ G and F is corepresentable, then G is corepresentable.

Русский

Корпредставляемость сохраняется при натуральном изоморфизме: если F ≅ G и F корпредставим, то G корпредставим.

LaTeX

$$$ F \\cong G \\land F.\\IsCorepresentable \\Rightarrow G.\\IsCorepresentable $$$

Lean4

theorem corepresentable_of_natIso (F : C ⥤ Type v₁) {G} (i : F ≅ G) [F.IsCorepresentable] : G.IsCorepresentable :=
  (F.corepresentableBy.ofIso i).isCorepresentable

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