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