mono_iff_isZero_kernel' — Mathlib

English

A reassociated version of sum_comp: (∑ f_j ≫ g_j) ≫ h = ∑ f_j ≫ g_j ≫ h.

Русский

Переприведённая версия: (∑ f_j ≫ g_j) ≫ h = ∑ f_j ≫ g_j ≫ h.

LaTeX

$$$\left(\sum_{j \in s} f_j \circ g_j\right) \circ h = \sum_{j \in s} (f_j \circ g_j \circ h)$$$

Lean4

theorem mono_iff_isZero_kernel' {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c) : Mono f ↔ IsZero c.pt :=
  ⟨fun _ ↦ KernelFork.IsLimit.isZero_of_mono hc, mono_of_isZero_kernel' c hc⟩

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