---

Step * of Lemma lg-edge-lg-connected

∀[T:Type]. ∀g:LabeledGraph(T). ∀a,b:ℕlg-size(g).  (lg-edge(g;a;b) ⇒ lg-connected(g;a;b))
BY
{ (Auto THEN Unfold `lg-connected` 0 THEN (BLemma `rel_plus_iff` THENM (Reduce 0 THEN With ⌜a⌝ (D 0)⋅)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}g:LabeledGraph(T).  \mforall{}a,b:\mBbbN{}lg-size(g).    (lg-edge(g;a;b)  {}\mRightarrow{}  lg-connected(g;a;b))


By

---

Latex:
(Auto
  THEN  Unfold  `lg-connected`  0
  THEN  (BLemma  `rel\_plus\_iff`  THENM  (Reduce  0  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (D  0)\mcdot{}))
  THEN  Auto)

---

Home Index