---

Step * 1 of Lemma satisfies-irr-face


1. I : fset(ℕ)
2. J : fset(ℕ)
3. as : fset(names(I))
4. bs : fset(names(I))
5. g : J ⟶ I
6. ∀[s:fset(Point(face_lattice(J)))]
     uiff(/\(s) = 1 ∈ Point(face_lattice(J));∀x:Point(face_lattice(J)). (x ∈ s ⇒ (x = 1 ∈ Point(face_lattice(J)))))
7. ∀x:Point(face_lattice(J)). (x ∈ <g>"(λa.(a=0)"(as)) ⇒ (x = 1 ∈ Point(face_lattice(J))))
8. ∀x:Point(face_lattice(J)). (x ∈ <g>"(λb.(b=1)"(bs)) ⇒ (x = 1 ∈ Point(face_lattice(J))))
9. a : names(I)
10. a ∈ as
⊢ (g a) = 0 ∈ Point(dM(J))
BY
{ (Thin (-3)
   THEN (RWO  "fset-image-compose" (-3)⋅ THENA Auto)
   THEN (RWO  "member-fset-image-iff" (-3) THENA Auto)
   THEN RepUR ``compose`` -3
   THEN (RWW "fl-morph-fl0 fl-morph-fl1" (-3) THENA Auto)) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. as : fset(names(I))
4. bs : fset(names(I))
5. g : J ⟶ I
6. ∀[s:fset(Point(face_lattice(J)))]
     uiff(/\(s) = 1 ∈ Point(face_lattice(J));∀x:Point(face_lattice(J)). (x ∈ s ⇒ (x = 1 ∈ Point(face_lattice(J)))))
7. ∀x:Point(face_lattice(J))
     ((↓∃x1:names(I). (x1 ∈ as ∧ (x = dM-to-FL(J;¬(g x1)) ∈ Point(face_lattice(J)))))
     ⇒ (x = 1 ∈ Point(face_lattice(J))))
8. a : names(I)
9. a ∈ as
⊢ (g a) = 0 ∈ Point(dM(J))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  as  :  fset(names(I))
4.  bs  :  fset(names(I))
5.  g  :  J  {}\mrightarrow{}  I
6.  \mforall{}[s:fset(Point(face\_lattice(J)))].  uiff(/\mbackslash{}(s)  =  1;\mforall{}x:Point(face\_lattice(J)).  (x  \mmember{}  s  {}\mRightarrow{}  (x  =  1)))
7.  \mforall{}x:Point(face\_lattice(J)).  (x  \mmember{}  <g>"(\mlambda{}a.(a=0)"(as))  {}\mRightarrow{}  (x  =  1))
8.  \mforall{}x:Point(face\_lattice(J)).  (x  \mmember{}  <g>"(\mlambda{}b.(b=1)"(bs))  {}\mRightarrow{}  (x  =  1))
9.  a  :  names(I)
10.  a  \mmember{}  as
\mvdash{}  (g  a)  =  0


By

---

Latex:
(Thin  (-3)
  THEN  (RWO    "fset-image-compose"  (-3)\mcdot{}  THENA  Auto)
  THEN  (RWO    "member-fset-image-iff"  (-3)  THENA  Auto)
  THEN  RepUR  ``compose``  -3
  THEN  (RWW  "fl-morph-fl0  fl-morph-fl1"  (-3)  THENA  Auto))

---

Home Index