Step
*
of Lemma
member-cubical-subset-I_cube
∀[I:fset(ℕ)]. ∀[psi:𝔽(I)]. ∀[J:fset(ℕ)]. ∀[f:J ⟶ I].  f ∈ I,psi(J) supposing (psi f) = 1
BY
{ (Auto THEN RepUR ``cubical-subset I_cube functor-ob rep-sub-sheaf cat-arrow names-cat`` 0 THEN MemTypeCD THEN Auto) }
Latex:
Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].    f  \mmember{}  I,psi(J)  supposing  (psi  f)  =  1
By
Latex:
(Auto
  THEN  RepUR  ``cubical-subset  I\_cube  functor-ob  rep-sub-sheaf  cat-arrow  names-cat``  0
  THEN  MemTypeCD
  THEN  Auto)
Home
Index