hasRightKanExtension — Mathlib

English

If there exists a pointwise right Kan extension E of F along L, then a right Kan extension of F along L exists (in particular, HasRightKanExtension L F).

Русский

Если существует точечное правое кан-расширение E F вдоль L, то существует правое кан-расширение F вдоль L (то есть HasRightKanExtension L F).

LaTeX

$$$\operatorname{HasRightKanExtension}(L,F)$$$

Lean4

theorem hasRightKanExtension : HasRightKanExtension L F :=
  have := h.isRightKanExtension
  HasRightKanExtension.mk E.left E.hom

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