instInitialInclLeftOfIsConnected — Mathlib

English

If C is connected, the left inclusion inclLeft C D : C ⥤ Join C D is an initial functor.

Русский

Если C связенa, то левое включение inclLeft C D : C ⥤ Join C D является начальным функтором.

LaTeX

$$$\mathrm{inclLeft}\colon C \to \mathrm{Join}(C,D)\text{ is initial when } C \text{ is connected}$$$

Lean4

instance [IsConnected C] : (inclLeft C D).Initial where
  out
    x :=
    match x with
    | .left _ => isConnected_of_isTerminal _ CostructuredArrow.mkIdTerminal
    | .right d => isConnected_of_equivalent (costructuredArrowEquiv C D d).symm

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