ofArrows_surj — Mathlib

English

If R = ofArrows Y f, then there exist i and h such that g = eqToHom(h) ≫ f i.

Русский

Если R = ofArrows Y f, то найдутся i и h such that g = eqToHom(h) ≫ f i.

LaTeX

$$$$\\text{If } R = \\mathrm{ofArrows}(Y,f), \\exists i, \\exists h: Y_i = Z \\land g = \\mathrm{eqToHom}(h) \\circ f_i.$$$$

Lean4

theorem ofArrows_surj {ι : Type*} {Y : ι → C} (f : ∀ i, Y i ⟶ X) {Z : C} (g : Z ⟶ X) (hg : ofArrows Y f g) :
    ∃ (i : ι) (h : Y i = Z), g = eqToHom h.symm ≫ f i :=
  by
  obtain ⟨i⟩ := hg
  exact ⟨i, rfl, by simp only [eqToHom_refl, id_comp]⟩

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