---

Step * of Lemma satisfies-irr-face

∀[I,J:fset(ℕ)]. ∀[as,bs:fset(names(I))]. ∀[g:J ⟶ I].
  uiff((irr_face(I;as;bs) g) = 1;(∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J)))))
  ∧ (∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``name-morph-satisfies irr_face`` 0
   THEN (RWW "fl-morph-fset-meet fset-image-union lattice-fset-meet-union" 0 THENA Auto)
   THEN (RWO "lattice-meet-eq-1" 0 THENA Auto)
   THEN (InstLemma  `lattice-fset-meet-is-1` [⌜face_lattice(J)⌝;⌜face_lattice-deq()⌝]⋅ THENA Auto)
   THEN RWO  "-1" 0
   THEN 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)). (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))

2
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. b : names(I)
10. b ∈ bs
⊢ (g b) = 1 ∈ Point(dM(J))

3
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. ∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J))))
8. ∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))
9. x : Point(face_lattice(J))
10. x ∈ <g>"(λa.(a=0)"(as))
⊢ x = 1 ∈ Point(face_lattice(J))

4
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. ∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J))))
8. ∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))
9. x : Point(face_lattice(J))
10. x ∈ <g>"(λb.(b=1)"(bs))
⊢ x = 1 ∈ Point(face_lattice(J))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[as,bs:fset(names(I))].  \mforall{}[g:J  {}\mrightarrow{}  I].
    uiff((irr\_face(I;as;bs)  g)  =  1;(\mforall{}a:names(I).  (a  \mmember{}  as  {}\mRightarrow{}  ((g  a)  =  0)))
    \mwedge{}  (\mforall{}b:names(I).  (b  \mmember{}  bs  {}\mRightarrow{}  ((g  b)  =  1))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``name-morph-satisfies  irr\_face``  0
  THEN  (RWW  "fl-morph-fset-meet  fset-image-union  lattice-fset-meet-union"  0  THENA  Auto)
  THEN  (RWO  "lattice-meet-eq-1"  0  THENA  Auto)
  THEN  (InstLemma    `lattice-fset-meet-is-1`  [\mkleeneopen{}face\_lattice(J)\mkleeneclose{};\mkleeneopen{}face\_lattice-deq()\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index