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