thinSkeletonOrderIso — Mathlib

English

The thin skeleton is equivalent to the original category via an explicit equivalence.

Русский

Тонкий скелет эквивалентен исходной категории через явную эквивалентность.

LaTeX

$$equivalence (ThinSkeleton C) ≃ C$$

Lean4

/-- When `e : C ≌ α` is a categorical equivalence from a thin category `C` to some partial order `α`,
the `ThinSkeleton C` is order isomorphic to `α`.
-/
noncomputable def thinSkeletonOrderIso [Quiver.IsThin C] (e : C ≌ α) : ThinSkeleton C ≃o α :=
  ((ThinSkeleton.equivalence C).trans e).toOrderIso

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