fac — Mathlib

English

The lift through the standard image factorisation equals the standard injection: image.lift {I := image f, m := ι f, e := factorThruImage f} ≫ image.ι f = image.ι f.

Русский

Поднятие через стандартную факторизацию образа равно стандартной инъекции: image.lift {I := image f, m := ι f, e := factorThruImage f} ≫ image.ι f = image.ι f.

LaTeX

$$$\mathrm{image.lift}\{ I := \mathrm{image} f,\ m := \iota f,\ e := \mathrm{factorThruImage} f \} \\; \\; \mathrm{image.\,ι} f = \mathrm{image.\,ι} f.$$$

Lean4

@[reassoc (attr := simp)]
theorem fac : factorThruImage f ≫ image.ι f = f :=
  (Image.monoFactorisation f).fac

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