---

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


1. T : Type
2. I : fset(ℕ)
3. as : fset(names(I))
4. bs : fset(names(I))
5. ↑fset-disjoint(NamesDeq;as;bs)
6. t : {I,irr_face(I;as;bs) ⊢ _:discr(T)}
7. {I,irr_face(I;as;bs) ⊢ _:discr(T)} ⊆r I,irr_face(I;as;bs) ij⟶ discrete-cube(T)
8. I,irr_face(I;as;bs) ij⟶ discrete-cube(T) ⊆r {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) = 1 ⇒ (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