hasLeftKanExtension — Mathlib

English

If HasLeftKanExtension f g holds, then LeftExtension f g has an initial object.

Русский

Если существует левое Кан-расширение f g, то у LeftExtension f g имеется начальный объект.

LaTeX

$$$[HasLeftKanExtension(f,g)] \Rightarrow \text{HasInitial}(\text{LeftExtension}(f,g)).$$$

Lean4

theorem hasLeftKanExtension {t : LeftExtension f g} (H : IsKan t) : HasLeftKanExtension f g :=
  ⟨IsInitial.hasInitial H⟩

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