Nuprl Definition : u-almost-full
u-almost-full(n.A[n]) == ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])
Definitions occuring in Statement :
strict-inc: StrictInc,
quotient: x,y:A//B[x; y],
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
true: True,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
strict-inc: StrictInc,
quotient: x,y:A//B[x; y],
exists: ∃x:A. B[x],
nat: ℕ,
apply: f a,
true: True
FDL editor aliases :
u-almost-full
Latex:
u-almost-full(n.A[n]) == \mforall{}s:StrictInc. \00D9(\mexists{}n:\mBbbN{}. A[s n])
Date html generated:
2016_05_14-PM-09_48_48
Last ObjectModification:
2015_12_18-PM-09_05_38
Theory : continuity
Home
Index