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