colimit_sound — Mathlib

English

If F.map f x = F.map f' x' for f: j → j'' and f': j' → j'' then colimit.ι F j x = colimit.ι F j' x'.

Русский

Если F.map f x = F.map f' x' для f: j → j'' и f': j' → j'' то colimit.ι F j x = colimit.ι F j' x'.

LaTeX

$$$$ \text{colimit.ι } F\ j\ x = \text{colimit.ι } F\ j'\ x' \quad \text{при } F.map f x = F.map f' x'. $$$$

Lean4

theorem colimit_sound {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : F.map f x = x') :
    colimit.ι F j x = colimit.ι F j' x' := by rw [← w, Colimit.w_apply]

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