isRepresentable_of_natIso — Mathlib

English

Representability is preserved under a natural isomorphism: if F ≅ G and F is representable, then G is representable.

Русский

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

LaTeX

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

Lean4

theorem isRepresentable_of_natIso (F : Cᵒᵖ ⥤ Type v₁) {G} (i : F ≅ G) [F.IsRepresentable] : G.IsRepresentable :=
  (F.representableBy.ofIso i).isRepresentable

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