---

Step * 5 of Lemma face_lattice-fset-join-eq-1


1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇒ (∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
5. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
6. ¬x ∈ s
7. ∃x@0:Point(face_lattice(I)). (x@0 ∈ fset-add(face_lattice-deq();x;s) ∧ (x@0 = 1 ∈ Point(face_lattice(I))))
⊢ \/(fset-add(face_lattice-deq();x;s)) = 1 ∈ Point(face_lattice(I))
BY
{ ((RepUR ``fset-add`` -1 THEN RepUR ``fset-add`` 0)
   THEN (RWW  "lattice-fset-join-union lattice-fset-join-singleton" 0 THENA Auto)
   THEN (RWO  "face_lattice-1-join-irreducible" 0 THENA Auto)
   THEN ExRepD) }

1
1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇒ (∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
5. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
6. ¬x ∈ s
7. x@0 : Point(face_lattice(I))
8. x@0 ∈ {x} ⋃ s
9. x@0 = 1 ∈ Point(face_lattice(I))
⊢ (x = 1 ∈ Point(face_lattice(I))) ∨ (\/(s) = 1 ∈ Point(face_lattice(I)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  s  :  fset(Point(face\_lattice(I)))
3.  x  :  Point(face\_lattice(I))
4.  (\mbackslash{}/(s)  =  1)  {}\mRightarrow{}  (\mexists{}x:Point(face\_lattice(I)).  (x  \mmember{}  s  \mwedge{}  (x  =  1)))
5.  (\mbackslash{}/(s)  =  1)  \mLeftarrow{}{}  \mexists{}x:Point(face\_lattice(I)).  (x  \mmember{}  s  \mwedge{}  (x  =  1))
6.  \mneg{}x  \mmember{}  s
7.  \mexists{}x@0:Point(face\_lattice(I)).  (x@0  \mmember{}  fset-add(face\_lattice-deq();x;s)  \mwedge{}  (x@0  =  1))
\mvdash{}  \mbackslash{}/(fset-add(face\_lattice-deq();x;s))  =  1


By

---

Latex:
((RepUR  ``fset-add``  -1  THEN  RepUR  ``fset-add``  0)
  THEN  (RWW    "lattice-fset-join-union  lattice-fset-join-singleton"  0  THENA  Auto)
  THEN  (RWO    "face\_lattice-1-join-irreducible"  0  THENA  Auto)
  THEN  ExRepD)

---

Home Index