---

Step * of Lemma cube-set-restriction-comp

No Annotations
∀X:j⊢. ∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I).  (g(f(a)) = f ⋅ g(a) ∈ X(K))
BY
{ PresheafMLTTInstance Obid: psc-restriction-comp⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:X(I).    (g(f(a))  =  f  \mcdot{}  g(a))


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-restriction-comp\mcdot{}

---

Home Index