---

Step * of Lemma lg-label-map

∀[f:Top]. ∀[g:LabeledGraph(Top)]. ∀[x:ℕlg-size(g)].  (lg-label(lg-map(f;g);x) ~ f lg-label(g;x))
BY
{ ((UnivCD THENA Auto) THEN Dlg (-2)) }

1
1. f : Top
2. g : LabeledGraph(Top)
3. lg-size(g) ∈ ℕ
4. g ∈ Top List
5. g ∈ (Top × ℕlg-size(g) List × (ℕlg-size(g) List)) List
6. x : ℕlg-size(g)
⊢ lg-label(lg-map(f;g);x) ~ f lg-label(g;x)

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[g:LabeledGraph(Top)].  \mforall{}[x:\mBbbN{}lg-size(g)].    (lg-label(lg-map(f;g);x)  \msim{}  f  lg-label(g;x))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Dlg  (-2))

---

Home Index