hasLeftKanExtension — Mathlib

English

If a pointwise left Kan extension exists, then a corresponding left Kan extension exists for the structure E.

Русский

Если существует точечное лево Кан-расширение, то существует соответствующее лево Кан-расширение для структуры E.

LaTeX

$$$\\text{HasLeftKanExtension}(L,F)$$$

Lean4

theorem hasLeftKanExtension : HasLeftKanExtension L F :=
  have := h.isLeftKanExtension
  HasLeftKanExtension.mk E.right E.hom

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