eHomEquiv — Mathlib

English

The bijection eHomEquiv is defined as the standard enriched hom equivalence.

Русский

Определяется биекция eHomEquiv как стандартная эквиваленция обогащённых гомоморфизмов.

LaTeX

$$$\mathrm{eHomEquiv} = \mathrm{EnrichedOrdinaryCategory.homEquiv}$.$$

Lean4

/-- The bijection `(X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y))` given by a
`EnrichedOrdinaryCategory` instance. -/
def eHomEquiv {X Y : C} : (X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y)) :=
  EnrichedOrdinaryCategory.homEquiv

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