condition — Mathlib

English

For f: F → F' and j ∈ J, the equation coend.map f ≫ coend.π F' j = coend.π F j ≫ (f.app (op j)).app j holds.

Русский

Для f: F → F' и j ∈ J выполняется coend.map f ≫ coend.π F' j = coend.π F j ≫ (f.app(op j)).app j.

LaTeX

$$$coend.map f \;≫\; coend.π F' j = coend.π F j \;≫\; (f.app { unop := j }).app j$$$

Lean4

@[reassoc]
theorem condition {i j : J} (f : i ⟶ j) : (F.map f.op).app i ≫ ι F i = (F.obj (op j)).map f ≫ ι F j := by
  apply Cowedge.condition

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