mk' — Mathlib

English

If there is an isomorphism coyoneda.obj(op X) ≅ F, then F is corepresentable.

Русский

Если существует изоморфизм coyoneda.obj(op X) ≅ F, то F корпредставимо.

LaTeX

$$$ F \\IsCorepresentable $$$

Lean4

/-- Alternative constructor for `F.IsCorepresentable`, which takes as an input an
isomorphism `coyoneda.obj (op X) ≅ F`. -/
theorem mk' {F : C ⥤ Type v₁} {X : C} (e : coyoneda.obj (op X) ≅ F) : F.IsCorepresentable :=
  (corepresentableByEquiv.symm e).isCorepresentable

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