Nuprl Definition : generic
Generic{f:ℕ⟶T|S[f]} ==
∃R:ℕ ⟶ (T List) ⟶ ℙ
((∀i:ℕ. ∀s:T List. ∃s':T List. (s ≤ s' ∧ (R i s')))
∧ (∀f:ℕ ⟶ T. ((∀i:ℕ. ∃s:T List. ((R i s) ∧ (∀n:ℕ||s||. (s[n] = (f n) ∈ T)))) ⇒ S[f])))
Definitions occuring in Statement :
iseg: l1 ≤ l2,
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
nat: ℕ,
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
prop: ℙ,
iseg: l1 ≤ l2,
function: x:A ⟶ B[x],
implies: P ⇒ Q,
nat: ℕ,
exists: ∃x:A. B[x],
list: T List,
and: P ∧ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
equal: s = t ∈ T,
select: L[n],
apply: f a
FDL editor aliases :
generic
Latex:
Generic\{f:\mBbbN{}{}\mrightarrow{}T|S[f]\} ==
\mexists{}R:\mBbbN{} {}\mrightarrow{} (T List) {}\mrightarrow{} \mBbbP{}
((\mforall{}i:\mBbbN{}. \mforall{}s:T List. \mexists{}s':T List. (s \mleq{} s' \mwedge{} (R i s')))
\mwedge{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} T. ((\mforall{}i:\mBbbN{}. \mexists{}s:T List. ((R i s) \mwedge{} (\mforall{}n:\mBbbN{}||s||. (s[n] = (f n))))) {}\mRightarrow{} S[f])))
Date html generated:
2016_05_15-PM-04_42_30
Last ObjectModification:
2015_09_23-AM-07_49_38
Theory : general
Home
Index