Nuprl Definition : ring-as-list
ring-as-list(T;L;f) == Inj({i:T| (i ∈ L)} ;{i:T| (i ∈ L)} ;f) ∧ (∀i,j:{i:T| (i ∈ L)} . ∃n:ℕ. (j = (f^n i) ∈ {i:T| (i ∈\000C L)} ))
Definitions occuring in Statement :
l_member: (x ∈ l),
fun_exp: f^n,
inject: Inj(A;B;f),
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
inject: Inj(A;B;f),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
nat: ℕ,
equal: s = t ∈ T,
set: {x:A| B[x]} ,
l_member: (x ∈ l),
apply: f a,
fun_exp: f^n
FDL editor aliases :
ring-as-list
Latex:
ring-as-list(T;L;f) == Inj(\{i:T| (i \mmember{} L)\} ;\{i:T| (i \mmember{} L)\} ;f) \mwedge{} (\mforall{}i,j:\{i:T| (i \mmember{} L)\} . \mexists{}n:\mBbbN{}. (j = \000C(f\^{}n i)))
Date html generated:
2016_05_15-PM-06_20_46
Last ObjectModification:
2015_09_23-AM-08_02_41
Theory : general
Home
Index