Nuprl Definition : all-large
∀large(n).P[n] == ∃N:ℕ. ∀n:ℕ. ((N ≤ n) ⇒ P[n])
Definitions occuring in Statement :
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
nat: ℕ,
implies: P ⇒ Q,
le: A ≤ B
FDL editor aliases :
all-large
Latex:
\mforall{}large(n).P[n] == \mexists{}N:\mBbbN{}. \mforall{}n:\mBbbN{}. ((N \mleq{} n) {}\mRightarrow{} P[n])
Date html generated:
2016_05_15-PM-05_29_09
Last ObjectModification:
2015_09_23-AM-07_54_32
Theory : general
Home
Index