Nuprl Definition : altunbounded
Unbounded(A) == ∀n:ℕ. ∃s:ℕn ⟶ T. (↑(A n s))
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-},
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
nat: ℕ,
all: ∀x:A. B[x]
FDL editor aliases :
altunbounded
Latex:
Unbounded(A) == \mforall{}n:\mBbbN{}. \mexists{}s:\mBbbN{}n {}\mrightarrow{} T. (\muparrow{}(A n s))
Date html generated:
2019_06_20-PM-02_46_04
Last ObjectModification:
2019_06_06-PM-01_24_25
Theory : fan-theorem
Home
Index