---

Step * of Lemma ext-equal-presheaves_wf

∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].  (ext-equal-presheaves(C;F;G) ∈ ℙ')
BY
{ ProveWfLemma }

1
1. C : SmallCategory
2. F : Presheaf(C)
3. G : Presheaf(C)
4. ∀x:cat-ob(C). ob(F) x ≡ ob(G) x
5. x : cat-ob(C)
6. y : cat-ob(C)
7. f : cat-arrow(C) y x
⊢ arrow(G) x y f ∈ (ob(F) x) ⟶ (ob(F) y)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F,G:Presheaf(C)].    (ext-equal-presheaves(C;F;G)  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index