---

Step * of Lemma continuous-ldag

∀[F:Type ⟶ Type]. Continuous+(T.LabeledDAG(F[T])) supposing Continuous+(T.F[T])
BY
{ (Auto
   THEN Unfold `ldag` 0
   THEN Using [`A',⌜LabeledGraph(Top)⌝] (BLemma `strong-continuous-set`)⋅
   THEN Auto
   THEN Try ((BLemma `continuous-labeled-graph` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  Continuous+(T.LabeledDAG(F[T]))  supposing  Continuous+(T.F[T])


By

---

Latex:
(Auto
  THEN  Unfold  `ldag`  0
  THEN  Using  [`A',\mkleeneopen{}LabeledGraph(Top)\mkleeneclose{}]  (BLemma  `strong-continuous-set`)\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `continuous-labeled-graph`  THEN  Auto)))

---

Home Index