initial_pre — Mathlib

English

If T is initial, then CostructuredArrow.pre T S X is initial for any S and X.

Русский

Если T начальная, то CostructuredArrow.pre T S X начальная.

LaTeX

$$$\operatorname{Initial}(T) \Rightarrow \operatorname{Initial}(\operatorname{CostructuredArrow.pre}(T,S,X))$$$

Lean4

/-- The functor `CostructuredArrow.pre X T S` is initial if `T` is initial. -/
instance initial_pre (T : C ⥤ D) [Initial T] (S : D ⥤ E) (X : E) : Initial (CostructuredArrow.pre T S X) :=
  by
  refine ⟨fun f => ?_⟩
  rw [isConnected_iff_of_equivalence (CostructuredArrow.preEquivalence T f)]
  exact Initial.out f.left

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