congr_hom

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.congr_hom

English

If f = g, then for every i, the i-th component satisfies f.f i = g.f i.

Русский

Если f = g, то для каждого i выполняется f.f i = g.f i.

LaTeX

$$$\\\\forall i \\\\; (f = g) \\\\Rightarrow f.f i = g.f i$$$

Lean4

theorem congr_hom {C D : HomologicalComplex V c} {f g : C ⟶ D} (w : f = g) (i : ι) : f.f i = g.f i :=
  congr_fun (congr_arg Hom.f w) i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru