Nuprl Definition : bij_inv
bij_inv(bi) == λb.(fst(((snd(bi)) b)))
Definitions occuring in Statement :
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
pi2: snd(t),
apply: f a,
pi1: fst(t),
lambda: λx.A[x]
FDL editor aliases :
bij_inv
Latex:
bij\_inv(bi) == \mlambda{}b.(fst(((snd(bi)) b)))
Date html generated:
2017_02_20-AM-10_47_55
Last ObjectModification:
2017_02_13-AM-10_53_59
Theory : list_1
Home
Index