instFinalInclRightOfIsConnected — Mathlib

English

If D is connected, the right inclusion inclRight C D : C ⥤ Join C D is a final functor.

Русский

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

LaTeX

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

Lean4

instance [IsConnected D] : (inclRight C D).Final where
  out
    x :=
    match x with
    | .left c => isConnected_of_equivalent (structuredArrowEquiv C D c).symm
    | .right _ => isConnected_of_isInitial _ (StructuredArrow.mkIdInitial (T := inclRight C D))

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