---

Step * of Lemma is-dag-map

∀[T,S:Type]. ∀[f:T ─→ S]. ∀[g:LabeledGraph(T)].  is-dag(lg-map(f;g)) supposing is-dag(g)
BY
{ (Auto
   THEN (InstLemma `lg-size-map` [⌈T⌉;⌈S⌉;⌈f⌉;⌈g⌉]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelOp -2)
   THEN RepeatFor 2 (ParallelLast)
   THEN FLemma `lg-edge-map` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].  \mforall{}[f:T  {}\mrightarrow{}  S].  \mforall{}[g:LabeledGraph(T)].    is-dag(lg-map(f;g))  supposing  is-dag(g)


By

---

Latex:
(Auto
  THEN  (InstLemma  `lg-size-map`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  FLemma  `lg-edge-map`  [-1]
  THEN  Auto)

---

Home Index