Nuprl Definition : extend-injection
extend-injection(a;f) == λx.if x <z a then f x else x fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a
FDL editor aliases :
extend-injection
Latex:
extend-injection(a;f) == \mlambda{}x.if x <z a then f x else x fi
Date html generated:
2018_05_21-PM-08_16_44
Last ObjectModification:
2017_12_15-AM-11_18_25
Theory : general
Home
Index