final_pre — Mathlib

English

The functor StructuredArrow.pre X T S is final if T is final.

Русский

Функтор StructuredArrow.pre X T S финален, если T финальная.

LaTeX

$$$\operatorname{Final}(T) \Rightarrow \operatorname{Final}(\operatorname{StructuredArrow.pre}(X,T,S))$$$

Lean4

/-- The functor `StructuredArrow.pre X T S` is final if `T` is final. -/
instance final_pre (T : C ⥤ D) [Final T] (S : D ⥤ E) (X : E) : Final (pre X T S) :=
  by
  refine ⟨fun f => ?_⟩
  rw [isConnected_iff_of_equivalence (StructuredArrow.preEquivalence T f)]
  exact Final.out f.right

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