kernelIsoOfEq_trans — Mathlib

English

Composition of two kernel iso of eq is equal to the kernelIsoOfEq of the combined equality.

Русский

Сложение изоморфизмов ядра по равенствам даёт KernelIsoOfEq от объединённого равенства.

LaTeX

$$$kernelIsoOfEq w_1 \\;\\circ\\; kernelIsoOfEq w_2 = kernelIsoOfEq (w_1 \\;\\text{trans}\\; w_2)$$$

Lean4

@[simp]
theorem kernelIsoOfEq_trans {f g h : X ⟶ Y} [HasKernel f] [HasKernel g] [HasKernel h] (w₁ : f = g) (w₂ : g = h) :
    kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (w₁.trans w₂) := by cases w₁; cases w₂; ext;
  simp [kernelIsoOfEq]

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