nonempty_indParallelPairPresentation

English

For any A,B that are Ind-objects and any morphisms f,g: A ⟶ B, the IndParallelPairPresentation f g exists (is nonempty).

Русский

Для любых A,B — ИнД-объекты и любых отображений f,g: A ⟶ B существует IndParallelPairPresentation f g (непуст).

LaTeX

$$$\text{Nonempty} (\mathrm{IndParallelPairPresentation}\; f\; g)$$$

Lean4

theorem nonempty_indParallelPairPresentation {A B : Cᵒᵖ ⥤ Type v₁} (hA : IsIndObject A) (hB : IsIndObject B)
    (f g : A ⟶ B) : Nonempty (IndParallelPairPresentation f g) :=
  ⟨NonemptyParallelPairPresentationAux.presentation f g hA.presentation hB.presentation⟩

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