imageSubobject_arrow' — Mathlib

English

The inverse of imageSubobjectIso f composed with imageSubobject f arrow equals the chosen image inclusion map image.ι f.

Русский

Обратная часть imageSubobjectIso f, применённая к стрелке imageSubobject f, равна image.ι f.

LaTeX

$$$(\mathrm{imageSubobjectIso} f).\mathrm{inv} \;\circ (\mathrm{imageSubobject} f).\mathrm{arrow} = \mathrm{image}.\mathrm{ι} f$$$

Lean4

@[reassoc (attr := simp)]
theorem imageSubobject_arrow' : (imageSubobjectIso f).inv ≫ (imageSubobject f).arrow = image.ι f := by
  simp [imageSubobjectIso]

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