Nuprl Definition : altjbar
jbar(X;Y) == ∀f:ℕ ⟶ T. ∀g:ℕ ⟶ S. ((∃n:ℕ. (↑(X n f))) ∨ (∃n:ℕ. (↑(Y n g))))
Definitions occuring in Statement :
nat: ℕ,
assert: ↑b,
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 :
apply: f a,
assert: ↑b,
nat: ℕ,
exists: ∃x:A. B[x],
or: P ∨ Q,
function: x:A ⟶ B[x],
all: ∀x:A. B[x]
FDL editor aliases :
altjbar
Latex:
jbar(X;Y) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mforall{}g:\mBbbN{} {}\mrightarrow{} S. ((\mexists{}n:\mBbbN{}. (\muparrow{}(X n f))) \mvee{} (\mexists{}n:\mBbbN{}. (\muparrow{}(Y n g))))
Date html generated:
2019_06_20-PM-02_46_11
Last ObjectModification:
2019_06_06-AM-10_48_11
Theory : fan-theorem
Home
Index