Nuprl Definition : sq-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],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q
Definitions occuring in definition :
sq_exists: ∃x:{A| B[x]},
all: ∀x:A. B[x],
nat: ℕ,
implies: P ⇒ Q,
le: A ≤ B
FDL editor aliases :
sq-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_41
Last ObjectModification:
2015_09_23-AM-07_54_39
Theory : general
Home
Index