explicitCokernelπ_desc_apply — Mathlib

English

explicitCokernelDesc(w)(explicitCokernelπ f(x)) = g(x).

Русский

explicitCokernelDesc(w) применено к explicitCokernelπ f(x) даёт g(x).

LaTeX

$$$explicitCokernelDesc(w)(explicitCokernel\\\\pi f\\\\, x) = g(x).$$$

Lean4

@[simp]
theorem explicitCokernelπ_desc_apply {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : f ≫ g = 0} (x : Y) :
    explicitCokernelDesc cond (explicitCokernelπ f x) = g x :=
  show (explicitCokernelπ f ≫ explicitCokernelDesc cond) x = g x by rw [explicitCokernelπ_desc]

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