---

Step * of Lemma co-regext-Regularcoset

∀a:coSet{i:l}. cRegular(co-regext(a))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (coSetD 1 THEN D 1 THEN All (Fold `mk-coset`))
   THEN Auto
   THEN (BLemma `co-regext-lemma` ⋅ THEN Auto)⋅) }

1
1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. B : coSet{i:l}
4. (B ∈ co-regext(mk-coset(T;a1)))
5. R : coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
6. coSetRelation(R)
7.  R:(B ⇒ co-regext(mk-coset(T;a1)))
⊢ ∃t:T. ∃g:set-dom(a1 t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(a1 t);g))

---

Latex:

---

Latex:
\mforall{}a:coSet\{i:l\}.  cRegular(co-regext(a))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (coSetD  1  THEN  D  1  THEN  All  (Fold  `mk-coset`))
  THEN  Auto
  THEN  (BLemma  `co-regext-lemma`  \mcdot{}  THEN  Auto)\mcdot{})

---

Home Index