Nuprl Definition : Spread-family
Spread-family(P;Pos;f;n,p,q.Mv[n; p; q]) == corec-family(λS,p. (a:Pos × (q:P ⟶ Mv[f a; p; q] ⟶ (S q))))
Definitions occuring in Statement :
corec-family: corec-family(H),
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
product: x:A × B[x]
Definitions occuring in definition :
corec-family: corec-family(H),
lambda: λx.A[x],
product: x:A × B[x],
function: x:A ⟶ B[x],
apply: f a
FDL editor aliases :
Spread-family
Latex:
Spread-family(P;Pos;f;n,p,q.Mv[n; p; q]) ==
corec-family(\mlambda{}S,p. (a:Pos \mtimes{} (q:P {}\mrightarrow{} Mv[f a; p; q] {}\mrightarrow{} (S q))))
Date html generated:
2016_05_14-PM-03_57_14
Last ObjectModification:
2015_09_22-PM-06_01_55
Theory : spread
Home
Index