hasLeftKanExtension — Mathlib

English

If F has a right derived functor, then F has a left Kan extension along L; this is a consequence of the equivalence with RightDerivedFunctor_iff.

Русский

Если у F есть правое производное, то у F существует левый Кан-расширение вдоль L; это следствие из эквивалентности с RightDerivedFunctor_iff.

LaTeX

$$HasLeftKanExtension L F$$

Lean4

theorem hasLeftKanExtension [HasRightDerivedFunctor F W] : HasLeftKanExtension L F := by
  simpa only [← hasRightDerivedFunctor_iff F L W]

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