---

Step * 1 of Lemma sub-presheaf-set_wf


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. P : I:cat-ob(C) ⟶ X(I) ⟶ ℙ{j'}
4. psc-predicate(C; X; I,rho.P[I;rho])
⊢ X|I,rho.P[I;rho] ∈ ps_context{j:l}(C)
BY
{ (InstLemma `presheaf-subset_wf1` [⌜parm{i}⌝;⌜parm{j'}⌝;⌜C⌝;⌜X⌝;⌜P⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  P  :  I:cat-ob(C)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  \mBbbP{}\{j'\}
4.  psc-predicate(C;  X;  I,rho.P[I;rho])
\mvdash{}  X|I,rho.P[I;rho]  \mmember{}  ps\_context\{j:l\}(C)


By

---

Latex:
(InstLemma  `presheaf-subset\_wf1`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{j'\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index