explicitCokernelIso_inv_π — Mathlib

English

For any X, Y in SemiNormedGrp and a morphism f: X ⟶ Y, the composition of cokernel.π f with the inverse of explicitCokernelIso f yields explicitCokernelπ f.

Русский

Для любых X, Y в SemiNormedGrp и морфизма f: X ⟶ Y, композиция cokernel.π f с обратной стороной explicitCokernelIso f даёт explicitCokernelπ f.

LaTeX

$$$ \mathrm{cokernel.π} f \circ (explicitCokernelIso f).inv = explicitCokernelπ f $$$

Lean4

@[simp]
theorem explicitCokernelIso_inv_π {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :
    cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f := by simp [explicitCokernelπ, explicitCokernelIso]

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