Nuprl Definition : baf-bar
baf-bar(n,m.R[n; m];n,m.T[n; m];l;a) ==
strictly-increasing-seq(l;a) ∧ (∃i:ℕl. ∃j,k:{i + 1..l-}. (R[a i; a j] ∧ T[a i; a k]))
Definitions occuring in Statement :
strictly-increasing-seq: strictly-increasing-seq(n;s),
int_seg: {i..j-},
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
add: n + m,
natural_number: $n
Definitions occuring in definition :
strictly-increasing-seq: strictly-increasing-seq(n;s),
exists: ∃x:A. B[x],
int_seg: {i..j-},
add: n + m,
natural_number: $n,
and: P ∧ Q,
apply: f a
FDL editor aliases :
baf-bar
Latex:
baf-bar(n,m.R[n; m];n,m.T[n; m];l;a) ==
strictly-increasing-seq(l;a) \mwedge{} (\mexists{}i:\mBbbN{}l. \mexists{}j,k:\{i + 1..l\msupminus{}\}. (R[a i; a j] \mwedge{} T[a i; a k]))
Date html generated:
2016_05_14-PM-09_51_24
Last ObjectModification:
2015_12_20-PM-06_09_08
Theory : continuity
Home
Index