comm_from — Mathlib

English

For a morphism f: C1.Hom C2 and any i, we have a commutativity relation at the From side: f.f i ≫ C2.dFrom i = C1.dFrom i ≫ f.next i.

Русский

Для морфизма f: C1.Hom C2 выполнено сопряжённое comm_from на стороне From: f.f i ≫ C2.dFrom i = C1.dFrom i ≫ f.next i.

LaTeX

$$$f.f i \\circ C_2.dFrom i = C_1.dFrom i \\circ f.next i$$$

Lean4

@[reassoc, elementwise]
theorem comm_from (f : Hom C₁ C₂) (i : ι) : f.f i ≫ C₂.dFrom i = C₁.dFrom i ≫ f.next i :=
  f.comm _ _

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