instSubsingleton — Mathlib

English

If γ1 = γ2 for RightHomologyMapData φ h1 h2, then γ1.φH = γ2.φH.

Русский

Если γ1 = γ2 для RightHomologyMapData φ h1 h2, тогда γ1.φH = γ2.φH.

LaTeX

$$$ \gamma_1 = \gamma_2 \Rightarrow \gamma_1.\phi_H = \gamma_2.\phi_H $$$

Lean4

instance : Subsingleton (RightHomologyMapData φ h₁ h₂) :=
  ⟨fun ψ₁ ψ₂ => by
    have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp]
    have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_mono h₂.ι, commι, commι, hQ]
    cases ψ₁
    cases ψ₂
    congr⟩

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