Nuprl Definition : jbar
jbar(T;S;X;Y) == ∀f:ℕ ⟶ T. ∀g:ℕ ⟶ S. ((∃n:ℕ. (X map(f;upto(n)))) ∨ (∃n:ℕ. (Y map(g;upto(n)))))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
or: P ∨ Q,
exists: ∃x:A. B[x],
nat: ℕ,
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
jbar
Latex:
jbar(T;S;X;Y) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mforall{}g:\mBbbN{} {}\mrightarrow{} S. ((\mexists{}n:\mBbbN{}. (X map(f;upto(n)))) \mvee{} (\mexists{}n:\mBbbN{}. (Y map(g;upto(n)))))
Date html generated:
2016_05_14-PM-04_09_12
Last ObjectModification:
2015_09_22-PM-06_02_15
Theory : fan-theorem
Home
Index