congr_left_φH

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.HomologyMapData.congr_left_φH

English

If two HomologyMapData γ1 and γ2 are equal, their left φH components are equal.

Русский

Если γ1 и γ2 совпадают, их левые φH-компоненты совпадают.

LaTeX

$$$ \gamma_1 = \gamma_2 \Rightarrow \gamma_1.left.φH = \gamma_2.left.φH $$$

Lean4

theorem congr_left_φH {γ₁ γ₂ : HomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.left.φH = γ₂.left.φH := by rw [eq]

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

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

Разделы

Аффилиация

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