toSkeleton_eq_iff — Mathlib

English

For X in C and Y in Skeleton C, toSkeleton X = Y iff there exists an isomorphism X ≅ (fromSkeleton C).obj Y.

Русский

Для X в C и Y в Skeleton C, toSkeleton X = Y тогда и только тогда, когда существует изоморфизм X ≅ (fromSkeleton C).obj Y.

LaTeX

$$$toSkeleton X = Y \iff \mathrm{Nonempty}(X \cong (\mathrm{fromSkeleton} C).obj Y)$$$

Lean4

theorem toSkeleton_eq_iff {X : C} {Y : Skeleton C} : toSkeleton X = Y ↔ Nonempty (X ≅ (fromSkeleton C).obj Y) :=
  Quotient.mk_eq_iff_out

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