---

Step * of Lemma subset-restriction

No Annotations
∀[X,Y:j⊢].  ∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[a:Y(I)].  (f(a) = f(a) ∈ X(J)) supposing sub_cubical_set{j:l}(Y; X)
BY
{ PresheafMLTTInstance Obid: ps-subset-restriction⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].
    \mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[a:Y(I)].    (f(a)  =  f(a))  supposing  sub\_cubical\_set\{j:l\}(Y;  X)


By

---

Latex:
PresheafMLTTInstance  Obid:  ps-subset-restriction\mcdot{}

---

Home Index