Nuprl Definition : per-product
per-product(A;a.B[a]) ==
pertype(λa,b. uand(ispair(a) ~ tt;uand(ispair(b) ~ tt;uand((fst(a)) = (fst(b)) ∈ A;(snd(a)) = (snd(b)) ∈ B[fst(a)]
supposing (fst(a))
= (fst(b))
∈ A))))
Definitions occuring in Statement :
uand: uand(A;B),
pertype: pertype(R),
bfalse: ff,
btrue: tt,
uimplies: b supposing a,
pi1: fst(t),
pi2: snd(t),
ispair: if z is a pair then a otherwise b,
lambda: λx.A[x],
sqequal: s ~ t,
equal: s = t ∈ T
Definitions occuring in definition :
pertype: pertype(R),
lambda: λx.A[x],
sqequal: s ~ t,
ispair: if z is a pair then a otherwise b,
bfalse: ff,
btrue: tt,
uand: uand(A;B),
uimplies: b supposing a,
equal: s = t ∈ T,
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
per-product
Latex:
per-product(A;a.B[a]) ==
pertype(\mlambda{}a,b. uand(ispair(a) \msim{} tt;uand(ispair(b) \msim{} tt;uand((fst(a))
= (fst(b));(snd(a)) = (snd(b)) supposing (fst(a)) = (fst(b))))))
Date html generated:
2016_05_13-PM-03_54_12
Last ObjectModification:
2015_09_22-PM-05_45_32
Theory : per!type
Home
Index