Nuprl Definition : lconnects
lconnects(p;i;j) ==
lpath(p)
∧ ((||p|| = 0 ∈ ℤ) ⇒ (i = j ∈ Id))
∧ ((¬(||p|| = 0 ∈ ℤ)) ⇒ ((i = source(hd(p)) ∈ Id) ∧ (j = destination(last(p)) ∈ Id)))
Definitions occuring in Statement :
lpath: lpath(p),
ldst: destination(l),
lsrc: source(l),
Id: Id,
last: last(L),
hd: hd(l),
length: ||as||,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
lconnects
lconnects(p;i;j) ==
lpath(p)
\mwedge{} ((||p|| = 0) {}\mRightarrow{} (i = j))
\mwedge{} ((\mneg{}(||p|| = 0)) {}\mRightarrow{} ((i = source(hd(p))) \mwedge{} (j = destination(last(p)))))
Date html generated:
2015_07_17-AM-09_12_34
Last ObjectModification:
2012_02_25-AM-10_53_07
Home
Index