instSubsingleton

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.HomologyMapData.instSubsingleton

← MathLib Explorer

English

If γ1 = γ2, then their left φH components are equal.

Русский

Если γ1 = γ2, то их левый компонент φH равен.

LaTeX

$$$ \gamma_1 = \gamma_2 \Rightarrow \gamma_1.left.\varphiH = \gamma_2.left.\varphiH $$$

Lean4

instance : Subsingleton (HomologyMapData φ h₁ h₂) :=
  ⟨by
    rintro ⟨left₁, right₁⟩ ⟨left₂, right₂⟩
    simp only [mk.injEq, eq_iff_true_of_subsingleton, and_self]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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