Nuprl Definition : decomp
decomp{i:l}(S.F[S];T;x) == con:Constr(T.F[T]) × {L:T List| ap-con(con;L) = x ∈ F[T]}
Definitions occuring in Statement :
ap-con: ap-con(con;L),
constructor: Constr(T.F[T]),
list: T List,
set: {x:A| B[x]} ,
product: x:A × B[x],
equal: s = t ∈ T
Definitions occuring in definition :
product: x:A × B[x],
constructor: Constr(T.F[T]),
set: {x:A| B[x]} ,
list: T List,
equal: s = t ∈ T,
ap-con: ap-con(con;L)
FDL editor aliases :
decomp
Latex:
decomp\{i:l\}(S.F[S];T;x) == con:Constr(T.F[T]) \mtimes{} \{L:T List| ap-con(con;L) = x\}
Date html generated:
2016_05_15-PM-06_56_04
Last ObjectModification:
2015_09_23-AM-08_07_56
Theory : general
Home
Index