mk_surjective — Mathlib

English

Every costructured arrow f: CostructuredArrow S T can be written as mk g for some Y and g: S.obj Y ⟶ T.

Русский

Каждый costructured arrow f: CostructuredArrow S T раскладывается как mk g для некоторого Y и g: S.obj Y ⟶ T.

LaTeX

$$$ \forall f : \mathrm{CostructuredArrow}(S,T), \exists Y:\, \exists g: S.obj Y \to T,\ f = \mathrm{mk} \; g.$$$

Lean4

theorem mk_surjective (f : CostructuredArrow S T) : ∃ (Y : C) (g : S.obj Y ⟶ T), f = mk g :=
  ⟨_, _, eq_mk f⟩

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