---

Step * 3 of Lemma name-morph-satisfies-fset-join


1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
⊢ ∀s:fset(Point(face_lattice(I))). ∀x:Point(face_lattice(I)).
    (((\/(s) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ s ∧ (a f) = 1))
    ⇒ (\/(fset-add(face_lattice-deq();x;s)) f) = 1
       ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ fset-add(face_lattice-deq();x;s) ∧ (a f) = 1) 
       supposing ¬x ∈ s)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``fset-add`` 0) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
4. s : fset(Point(face_lattice(I)))
5. x : Point(face_lattice(I))
6. (\/(s) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ s ∧ (a f) = 1)
7. ¬x ∈ s
⊢ (\/({x} ⋃ s) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ {x} ⋃ s ∧ (a f) = 1)

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  f  :  J  {}\mrightarrow{}  I
\mvdash{}  \mforall{}s:fset(Point(face\_lattice(I))).  \mforall{}x:Point(face\_lattice(I)).
        (((\mbackslash{}/(s)  f)  =  1  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}a:Point(face\_lattice(I)).  (a  \mmember{}  s  \mwedge{}  (a  f)  =  1))
        {}\mRightarrow{}  (\mbackslash{}/(fset-add(face\_lattice-deq();x;s))  f)  =  1
              \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}a:Point(face\_lattice(I)).  (a  \mmember{}  fset-add(face\_lattice-deq();x;s)  \mwedge{}  (a  f)  =  1) 
              supposing  \mneg{}x  \mmember{}  s)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``fset-add``  0)

---

Home Index