lift_mk_factorThruImage — Mathlib

English

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

Русский

Поднятие через каноническую факторизацию изображения равно каноническому включению: image.lift { ... } ≫ image.ι f = image.ι f.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem lift_mk_factorThruImage :
    image.lift { I := image f, m := ι f, e := factorThruImage f } ≫ image.ι f = image.ι f :=
  (Image.isImage f).lift_fac _

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