colimit_mul_mk_eq' — Mathlib

English

For any j ∈ J and x, y ∈ F.obj j, the product of the two canonical representatives equals the canonical representative with the product x*y at the same index j.

Русский

Для любого j ∈ J и элементов x,y ∈ F.obj j произведение двух канонических представителей равно каноническому представителю с произведением x*y на том же индексе j.

LaTeX

$$$G.mk F \langle j, x \rangle * G.mk F \langle j, y \rangle = G.mk F \langle j, x * y \rangle$$$

Lean4

@[to_additive]
theorem colimit_mul_mk_eq' {j : J} (x y : F.obj j) :
    G.mk.{v, u} F ⟨j, x⟩ * G.mk.{v, u} F ⟨j, y⟩ = G.mk.{v, u} F ⟨j, x * y⟩ := by
  simpa using colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)

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