ιMapBifunctorOrZero_eq_zero — Mathlib

English

Defines the inclusion of a summand of the j-th component of the map bifunctor between two complexes.

Русский

Определяет включение сумманду j-го компонента двойного отображения между двумя комплексами.

LaTeX

$$def ιMapBifunctor : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (mapBifunctor K₁ K₂ F c).X j$$

Lean4

theorem ιMapBifunctorOrZero_eq_zero (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) ≠ j) :
    ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂ j = 0 :=
  dif_neg h

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