kernel_from_eq_kernel — Mathlib

English

For HasKernels V, and any i, j with r: c.Rel i j, kernel of dFrom i equals kernel of d i j.

Русский

Для HasKernels V и любых i, j с r: c.Rel i j, ядро dFrom i совпадает с ядром d i j.

LaTeX

$$$\\\\text{kernelSubobject}(C.dFrom i) = \\\\text{kernelSubobject}(C.d i j)$$$

Lean4

theorem kernel_from_eq_kernel [HasKernels V] {i j : ι} (r : c.Rel i j) :
    kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j) :=
  by
  rw [C.dFrom_eq r]
  apply kernelSubobject_comp_mono

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