kernelIsoOfEq_refl — Mathlib

English

The inverse of kernelIsoOfEq commutes with the kernel inclusion: (kernelIsoOfEq h).inv ≫ ker.ι = ker.ι.

Русский

Обратный к kernelIsoOfEq помещает композицию с инъекцией ядра в исходную инъекцию: (kernelIsoOfEq h).inv ≫ ker.ι = ker.ι.

LaTeX

$$$\\bigl(\\kerIsoOfEq(h)\\bigr)^{-1} \\circ \\ker\\iota_{f} = \\ker\\iota_{g}$, где $h: f=g$.$$

Lean4

@[simp]
theorem kernelIsoOfEq_refl {h : f = f} : kernelIsoOfEq h = Iso.refl (kernel f) :=
  by
  ext
  simp [kernelIsoOfEq]

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