kernelIsoOfEq_inv_comp_ι — Mathlib

English

Alternative expression of the inv-comp with kernel inclusion when f=g.

Русский

Альтернативное выражение инверсной композиции с инъекцией ядра при f=g.

LaTeX

$$$(\\kerIsoOfEq(h)).inv ≫ \\ker.ι = \\ker.ι$ для h: f=g$$$

Lean4

@[reassoc (attr := simp)]
theorem kernelIsoOfEq_inv_comp_ι {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) :
    (kernelIsoOfEq h).inv ≫ kernel.ι _ = kernel.ι _ := by subst h; simp

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