imageSubobject_arrow_comp — Mathlib

English

The composition factorThruImageSubobject f ≫ (imageSubobject f).arrow equals f.

Русский

Составление factorThruImageSubobject f с arrow-subobject imageSubobject f даёт ровно f.

LaTeX

$$$\mathrm{factorThruImageSubobject} f \;\gg\; (\mathrm{imageSubobject} f).\mathrm{arrow} = f$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem imageSubobject_arrow_comp : factorThruImageSubobject f ≫ (imageSubobject f).arrow = f := by
  simp [factorThruImageSubobject]

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