objAsTypeEquiv — Mathlib

English

The constructed category AsType α is equivalent to α via an explicit equivalence.

Русский

Сконструированная категория AsType α эквивалентна α через явную эквивалентность.

LaTeX

$$$\\AsType(\\alpha) \\simeq \\alpha$$$

Lean4

/-- The constructed category is indeed equivalent to `α`. -/
noncomputable def objAsTypeEquiv : ObjAsType α ≌ α :=
  (inducedFunctor (Fintype.equivFin α).symm).asEquivalence

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