mk' — Mathlib

English

There exists a canonical right Kan extension for L and F.

Русский

Существует каноничное правое кан-расширение для L и F.

LaTeX

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

Lean4

/-- Alternative constructor for `PreservesLeftKanExtension`, phrased in terms of
`LeftExtension.IsUniversal` instead. See `PreservesLeftKanExtension.mk_of_preserves_isUniversal`
for a similar constructor taking as input a single `LeftExtension`. -/
theorem mk'
    (preserves :
      ∀ {E : LeftExtension L F}, E.IsUniversal → Nonempty (LeftExtension.postcompose₂ L F G |>.obj E).IsUniversal) :
    G.PreservesLeftKanExtension F L where
  preserves _ _
    h :=
    ⟨⟨Limits.IsInitial.equivOfIso (LeftExtension.postcompose₂ObjMkIso _ _) <|
          (preserves h.nonempty_isUniversal.some).some⟩⟩

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