imageSubobject_le_mk — Mathlib

English

Given a mono g: X → B and f: A → B with HasImage f, and h: A → X such that f = h ≫ g, then imageSubobject f ≤ Subobject.mk g.

Русский

Пусть $g: X\\to B$ моно, $f: A\\to B$ имеют образ, и $h: A\\to X$ удовлетворяет $f = h\\circ g$. Тогда $\\mathrm{imageSubobject}(f) \\le \\mathrm{Subobject.mk}\, g$.

LaTeX

$$$g: X \\to B$ mono, $f: A \\to B$, HasImage f, $h: A \\to X$, $w: h \\circ X.arrow = f$ gives $\\mathrm{imageSubobject}(f) \\le \\mathrm{Subobject.mk}\, g$.$$

Lean4

theorem imageSubobject_le_mk {A B : C} {X : C} (g : X ⟶ B) [Mono g] (f : A ⟶ B) [HasImage f] (h : A ⟶ X)
    (w : h ≫ g = f) : imageSubobject f ≤ Subobject.mk g :=
  imageSubobject_le f (h ≫ (Subobject.underlyingIso g).inv) (by simp [w])

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