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