instSubsingleton — Mathlib

English

For fixed φ : S1 → S2 and left-homology data h1, h2, there is at most one LeftHomologyMapData φ h1 h2.

Русский

Для заданного φ: S1 → S2 и данных левой гомологии h1, h2 существует не более одного LeftHomologyMapData φ h1 h2.

LaTeX

$$Subsingleton (LeftHomologyMapData φ h1 h2)$$

Lean4

instance : Subsingleton (LeftHomologyMapData φ h₁ h₂) :=
  ⟨fun ψ₁ ψ₂ => by
    have hK : ψ₁.φK = ψ₂.φK := by rw [← cancel_mono h₂.i, commi, commi]
    have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_epi h₁.π, commπ, commπ, hK]
    cases ψ₁
    cases ψ₂
    congr⟩

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