Step * 1 of Lemma discrete-cubical-term-is-constant-on-irr-face


1. Type
2. fset(ℕ)
3. as fset(names(I))
4. bs fset(names(I))
5. ↑fset-disjoint(NamesDeq;as;bs)
6. {I,irr_face(I;as;bs) ⊢ _:discr(T)}
7. {I,irr_face(I;as;bs) ⊢ _:discr(T)} ⊆I,irr_face(I;as;bs) ij⟶ discrete-cube(T)
8. I,irr_face(I;as;bs) ij⟶ discrete-cube(T) ⊆{I,irr_face(I;as;bs) ⊢ _:discr(T)}
9. irr-face-morph(I;as;bs) ∈ {f:I ⟶ I| (irr_face(I;as;bs) f) 1} 
⊢ ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((irr_face(I;as;bs) g)  (g irr-face-morph(I;as;bs) ⋅ g ∈ J ⟶ I))
BY
(Intros THEN BLemma `irr-face-morph-property` THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  I  :  fset(\mBbbN{})
3.  as  :  fset(names(I))
4.  bs  :  fset(names(I))
5.  \muparrow{}fset-disjoint(NamesDeq;as;bs)
6.  t  :  \{I,irr\_face(I;as;bs)  \mvdash{}  \_:discr(T)\}
7.  \{I,irr\_face(I;as;bs)  \mvdash{}  \_:discr(T)\}  \msubseteq{}r  I,irr\_face(I;as;bs)  ij{}\mrightarrow{}  discrete-cube(T)
8.  I,irr\_face(I;as;bs)  ij{}\mrightarrow{}  discrete-cube(T)  \msubseteq{}r  \{I,irr\_face(I;as;bs)  \mvdash{}  \_:discr(T)\}
9.  irr-face-morph(I;as;bs)  \mmember{}  \{f:I  {}\mrightarrow{}  I|  (irr\_face(I;as;bs)  f)  =  1\} 
\mvdash{}  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[g:J  {}\mrightarrow{}  I].    ((irr\_face(I;as;bs)  g)  =  1  {}\mRightarrow{}  (g  =  irr-face-morph(I;as;bs)  \mcdot{}  g))


By


Latex:
(Intros  THEN  BLemma  `irr-face-morph-property`  THEN  Auto)




Home Index