mem_im_iff — Mathlib

English

f ∈ (im φ hφ).arrows c d iff there exist a,b,g,ha,hb with f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb.

Русский

f принадлежит im φ hφ .arrows тогда и только тогда, когда существует a,b,g,ha,hb такие, что f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb.

LaTeX

$$$f \in (im φ hφ).arrows c d \iff \\exists a,b,g,ha,hb:\ f = eqToHom ha.symm \gg φ.map g \gg eqToHom hb$$$

Lean4

theorem mem_im_iff (hφ : Function.Injective φ.obj) {c d : D} (f : c ⟶ d) :
    f ∈ (im φ hφ).arrows c d ↔
      ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb :=
  by convert Map.arrows_iff φ hφ ⊤ f; simp only [Top.top, mem_univ, exists_true_left]

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