Nuprl Definition : adjacent
adjacent(T;L;x;y) == ∃i:ℕ||L|| - 1. ((x = L[i] ∈ T) ∧ (y = L[i + 1] ∈ T))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
exists: ∃x:A. B[x],
and: P ∧ Q,
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
int_seg: {i..j-},
subtract: n - m,
length: ||as||,
and: P ∧ Q,
equal: s = t ∈ T,
select: L[n],
add: n + m,
natural_number: $n
FDL editor aliases :
adjacent
Latex:
adjacent(T;L;x;y) == \mexists{}i:\mBbbN{}||L|| - 1. ((x = L[i]) \mwedge{} (y = L[i + 1]))
Date html generated:
2016_05_15-PM-03_36_51
Last ObjectModification:
2015_09_23-AM-07_44_19
Theory : general
Home
Index