d₁_eq' — Mathlib

English

Extensional equality for maps out of a bifunctor: two morphisms are equal if their compositions with each ιMapBifunctor agree.

Русский

Экстенциальное равенство отображений из двойственного: два морфизма равны, если их композиции с каждым ιMapBifunctor совпадают.

LaTeX

$$hom_ext {Y} {j} {f g} (h) : f = g$$

Lean4

theorem d₁_eq' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) :
    d₁ K₁ K₂ F c i₁ i₂ j =
      ComplexShape.ε₁ c₁ c₂ c ⟨i₁, i₂⟩ •
        ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ ιMapBifunctorOrZero K₁ K₂ F c i₁' i₂ j) :=
  HomologicalComplex₂.d₁_eq' _ _ h _ _

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