fullyFaithfulUncurry₃ — Mathlib

English

The uncurry operation in three variables is a fully faithful functor

Русский

Операция раскурривания в трёх переменных образует полностью верный функтор

LaTeX

$$$\text{fullyFaithfulUncurry}_3 : (\operatorname{uncurry}_3) : \mathsf{Fun}(C_1, \mathsf{Fun}(C_2, \mathsf{Fun}(C_3, E))) \to \mathsf{Fun}(C_1 \times C_2 \times C_3, E)$ is FullyFaithful$$

Lean4

/-- Uncurrying functors in three variables gives a fully faithful functor. -/
def fullyFaithfulUncurry₃ : (uncurry₃ : (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ (C₁ × C₂ × C₃ ⥤ E)).FullyFaithful :=
  currying₃.fullyFaithfulFunctor

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