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