---

Step * of Lemma continuous-labeled-graph

∀[F:Type ⟶ Type]. Continuous+(T.LabeledGraph(F[T])) supposing Continuous+(T.F[T])
BY
{ (Unfold `labeled-graph` 0 THEN (Auto THEN BLemma `strong-continuous-dep-isect` THEN Auto)) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `labeled-graph`  0  THEN  (Auto  THEN  BLemma  `strong-continuous-dep-isect`  THEN  Auto))

---

Home Index