---

Step * of Lemma cubical-subset-I_cube-member

∀[I:fset(ℕ)]. ∀[psi:𝔽(I)]. ∀[J:fset(ℕ)]. ∀[f:I,psi(J)].  ((f ∈ J ⟶ I) ∧ (psi f) = 1)
BY
{ (Auto
   THEN OnVar `f' (\h. (RepUR ``cubical-subset I_cube functor-ob rep-sub-sheaf cat-arrow names-cat`` h
                        THEN D h
                        THEN Auto
                        THEN All (RepUR ``name-morph-satisfies``)
                        THEN Auto))⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[f:I,psi(J)].    ((f  \mmember{}  J  {}\mrightarrow{}  I)  \mwedge{}  (psi  f)  =  1)


By

---

Latex:
(Auto
  THEN  OnVar  `f'  (\mbackslash{}h.  (RepUR  ``cubical-subset  I\_cube  functor-ob  rep-sub-sheaf  cat-arrow  names-cat``  h
                                            THEN  D  h
                                            THEN  Auto
                                            THEN  All  (RepUR  ``name-morph-satisfies``)
                                            THEN  Auto))\mcdot{}
  )

---

Home Index