---

Step * of Lemma irr-face-morph-property

No Annotations
∀[I:fset(ℕ)]. ∀[as,bs:fset(names(I))]. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].
  ((irr_face(I;as;bs) g) = 1 ⇒ (g = irr-face-morph(I;as;bs) ⋅ g ∈ J ⟶ I))
BY
{ (Auto
   THEN (RWO  "satisfies-irr-face" (-1) THENA Auto)
   THEN D -1
   THEN NameMorphExt
   THEN RepUR ``irr-face-morph`` 0
   THEN Repeat (AutoSplit)) }

1
1. I : fset(ℕ)
2. as : fset(names(I))
3. bs : fset(names(I))
4. J : fset(ℕ)
5. g : J ⟶ I
6. ∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J))))
7. ∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))
8. x : names(I)
9. x ∈ as
⊢ (g x) = (dM-lift(J;I;g) 0) ∈ Point(dM(J))

2
1. I : fset(ℕ)
2. as : fset(names(I))
3. bs : fset(names(I))
4. J : fset(ℕ)
5. g : J ⟶ I
6. ∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J))))
7. ∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))
8. x : names(I)
9. ¬x ∈ as
10. x ∈ bs
⊢ (g x) = (dM-lift(J;I;g) 1) ∈ Point(dM(J))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[as,bs:fset(names(I))].  \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:
(Auto
  THEN  (RWO    "satisfies-irr-face"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  NameMorphExt
  THEN  RepUR  ``irr-face-morph``  0
  THEN  Repeat  (AutoSplit))

---

Home Index