---

Step * of Lemma comem-graph-cosets

∀[I:Type]. ∀[E:I ⟶ I ⟶ ℙ].
  ∀i:I. ∀x:coSet{i:l}.
    (comem{i:l}(x;graph-cosets(I;i,j.E[i;j]) i) ⇐⇒ ∃j:I. (E[i;j] ∧ (x = (graph-cosets(I;i,j.E[i;j]) j) ∈ coSet{i:l})))
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] (UnfoldC `graph-cosets`)) 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Fold `graph-cosets` 0
   THEN RepUR ``comem set-dom set-item`` 0
   THEN Auto
   THEN ExRepD) }

1
1. [I] : Type
2. [E] : I ⟶ I ⟶ ℙ
3. i : I
4. x : coSet{i:l}
5. t : j:I × E[i;j]
6. x = (graph-cosets(I;i,j.E[i;j]) (fst(t))) ∈ coSet{i:l}
⊢ ∃j:I. (E[i;j] ∧ (x = (graph-cosets(I;i,j.E[i;j]) j) ∈ coSet{i:l}))

2
1. [I] : Type
2. [E] : I ⟶ I ⟶ ℙ
3. i : I
4. x : coSet{i:l}
5. j : I
6. E[i;j]
7. x = (graph-cosets(I;i,j.E[i;j]) j) ∈ coSet{i:l}
⊢ ∃t:j:I × E[i;j]. (x = (graph-cosets(I;i,j.E[i;j]) (fst(t))) ∈ coSet{i:l})

---

Latex:

---

Latex:
\mforall{}[I:Type].  \mforall{}[E:I  {}\mrightarrow{}  I  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}i:I.  \mforall{}x:coSet\{i:l\}.
        (comem\{i:l\}(x;graph-cosets(I;i,j.E[i;j])  i)
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}j:I.  (E[i;j]  \mwedge{}  (x  =  (graph-cosets(I;i,j.E[i;j])  j))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  (UnfoldC  `graph-cosets`))  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Fold  `graph-cosets`  0
  THEN  RepUR  ``comem  set-dom  set-item``  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index