---

Step * of Lemma irr-face-morph-satisfies

∀[I:fset(ℕ)]. ∀[as,bs:fset(names(I))].
  (irr_face(I;as;bs) irr-face-morph(I;as;bs)) = 1 supposing ↑fset-disjoint(NamesDeq;as;bs)
BY
{ (Auto THEN BLemma `satisfies-irr-face` THEN Auto THEN RepUR ``irr-face-morph`` 0 THEN AutoSplit) }

1
1. I : fset(ℕ)
2. as : fset(names(I))
3. bs : fset(names(I))
4. ↑fset-disjoint(NamesDeq;as;bs)
5. ∀a:names(I). (a ∈ as ⇒ ((irr-face-morph(I;as;bs) a) = 0 ∈ Point(dM(I))))
6. b : names(I)
7. b ∈ bs
8. b ∈ as
⊢ 0 = 1 ∈ Point(dM(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[as,bs:fset(names(I))].
    (irr\_face(I;as;bs)  irr-face-morph(I;as;bs))  =  1  supposing  \muparrow{}fset-disjoint(NamesDeq;as;bs)


By

---

Latex:
(Auto  THEN  BLemma  `satisfies-irr-face`  THEN  Auto  THEN  RepUR  ``irr-face-morph``  0  THEN  AutoSplit)

---

Home Index