ι_desc — Mathlib

English

Let g : WidePushout B objs arrows → X. If ∀ j, ι arrows j ≫ g = fs j and head arrows ≫ g = f, then g = desc f fs w.

Русский

Пусть g : WidePushout B objs arrows → X. Если для всех j верно ι arrows j ≫ g = fs j и head arrows ≫ g = f, то g = desc f fs w.

LaTeX

$$$\\big( \\forall j:\\, J,\\; ι arrows j \\;\\circ\\; g = fs j \\big) \\to\\; ( head arrows \\circ g = f ) \\to\\; g = \\mathrm{desc}(f,fs,w).$$$

Lean4

@[reassoc]
theorem ι_desc (j : J) : ι arrows j ≫ desc f fs w = fs _ := by
  simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

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