preservesLimit_curriedTensor — Mathlib

English

If for every c in C the functor F preserves limits after tensoring on the right by c, then F preserves the curried tensor product curriedTensor C.

Русский

Если для каждого c в C F сохраняет пределы после тензорирования справа на c, тогда F сохраняет curriedTensor C.

LaTeX

$$$[h := \\forall c : C, PreservesLimit F (tensorRight c)] \\Rightarrow PreservesLimit F (curriedTensor C)$$$

Lean4

theorem preservesLimit_curriedTensor [h : ∀ c : C, PreservesLimit F (tensorRight c)] :
    PreservesLimit F (curriedTensor C) :=
  preservesLimit_of_evaluation _ _ <| fun c ↦ inferInstanceAs (PreservesLimit F (tensorRight c))

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