le_mk_of_comm — Mathlib

English

If there exists a morphism g: A → X with g ≫ f = X.arrow, then X ≤ mk f.

Русский

Если существует г: A → X такой, что g ≫ f = X.arrow, то X ≤ mk f.

LaTeX

$$$\\exists g: A \\to X \\; (g \\gg f = X.arrow) \\Rightarrow X \\le mk f$$$

Lean4

theorem le_mk_of_comm {B A : C} {X : Subobject B} {f : A ⟶ B} [Mono f] (g : (X : C) ⟶ A) (w : g ≫ f = X.arrow) :
    X ≤ mk f :=
  le_of_comm (g ≫ (underlyingIso f).inv) <| by simp [w]

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