Nuprl Definition : subsequence
subsequence(a,b.E[a; b];m.x[m];n.y[n]) ==  ∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ E[y[n]; x[m]]) supposing N ≤ n
Definitions occuring in Statement : 
nat: ℕ
, 
uimplies: b supposing a
, 
le: A ≤ B
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
uimplies: b supposing a
, 
exists: ∃x:A. B[x]
, 
nat: ℕ
, 
and: P ∧ Q
, 
le: A ≤ B
FDL editor aliases : 
subsequence
Latex:
subsequence(a,b.E[a;  b];m.x[m];n.y[n])  ==
    \mexists{}N:\mBbbN{}.  \mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  ((n  \mleq{}  m)  \mwedge{}  E[y[n];  x[m]])  supposing  N  \mleq{}  n
Date html generated:
2019_06_20-PM-00_31_46
Last ObjectModification:
2019_04_22-PM-01_46_30
Theory : relations
Home
Index