mk' — Mathlib

English

An alternative constructor for PreservesRightKanExtension via universality of a postcomposition.

Русский

Альтернативный конструктор PreservesRightKanExtension через универсальность постсочетания.

LaTeX

$$$\text{PreservesRightKanExtension.mk'}$$$

Lean4

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

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