isPullback_initial_to_sigma_ι — Mathlib

English

A variant formulation stating the pullback of initial maps with respect to Sigma.ι indexed by i and j.

Русский

Вариант формулировки для пуллбека начальных отображений относительно Sigma.ι индексируемого i и j.

LaTeX

$$IsPullback( initial.to X_i, initial.to X_j, Sigma.ι X i, Sigma.ι X j )$$

Lean4

theorem isPullback_initial_to_sigma_ι [FinitaryExtensive C] {ι : Type*} [Finite ι] (X : ι → C) (i j : ι) (e : i ≠ j) :
    IsPullback (initial.to _) (initial.to _) (Sigma.ι X i) (Sigma.ι X j) :=
  FinitaryExtensive.isPullback_initial_to (coproductIsCoproduct _) ⟨i⟩ ⟨j⟩ (ne_of_apply_ne Discrete.as e)

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