---

Step * of Lemma csm-ap_wf

No Annotations
∀[X,Y:j⊢]. ∀[s:X j⟶ Y]. ∀[I:fset(ℕ)]. ∀[x:X(I)].  ((s)x ∈ Y(I))
BY
{ PresheafMLTTInstance Obid: pscm-ap_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].  \mforall{}[s:X  j{}\mrightarrow{}  Y].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:X(I)].    ((s)x  \mmember{}  Y(I))


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-ap\_wf\mcdot{}

---

Home Index