ι_desc_apply — Mathlib

English

For a cocone s over F and any j ∈ J and x ∈ F(j), the universal description desc F s applied to colimit.ι F j x equals s.ι.app j x.

Русский

Для кокона s над F и любого j ∈ J и x ∈ F(j) отображение desc F s на colimit.ι F j x равно s.ι.app j x.

LaTeX

$$$$ \text{colimit.desc } F\ s\ (\text{colimit.}\iota F\ j\ x) = s.\iota.\app j\ x. $$$$

Lean4

@[simp]
theorem ι_desc_apply (s : Cocone F) (j : J) (x : F.obj j) : colimit.desc F s (colimit.ι F j x) = s.ι.app j x :=
  congr_fun (colimit.ι_desc s j) x

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