Nuprl Definition : altbar
bar(X) == ∀f:ℕ ⟶ T. ∃n:ℕ. (↑(X n f))
Definitions occuring in Statement :
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
apply: f a,
assert: ↑b,
nat: ℕ,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
all: ∀x:A. B[x]
FDL editor aliases :
altbar
Latex:
bar(X) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}. (\muparrow{}(X n f))
Date html generated:
2019_06_20-PM-02_45_54
Last ObjectModification:
2019_06_06-AM-10_46_00
Theory : fan-theorem
Home
Index