instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit

English

The counit of the pointwise right Kan extension exhibits a right Kan extension.

Русский

Сопровождающий натуралной трансформации направленного кан-расширения образует правое кан-расширение.

LaTeX

$$$\operatorname{IsRightKanExtension}(\text{pointwiseRightKanExtensionCounit}(L,F))$$$

Lean4

instance : (pointwiseRightKanExtension L F).IsRightKanExtension (pointwiseRightKanExtensionCounit L F) where
  nonempty_isUniversal := ⟨pointwiseRightKanExtensionIsUniversal L F⟩

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