Nuprl Definition : per-union
per-union(A;B) ==
pertype(λa,b. uand(uand((a)↓;(b)↓);if a is inl then if b is inl then outl(a) = outl(b) ∈ A
else per-void()
else if a is inr then if b is inr then outr(a) = outr(b) ∈ B
else per-void()
else per-void()
supposing uand((a)↓;(b)↓)))
Definitions occuring in Statement :
per-void: per-void(),
uand: uand(A;B),
pertype: pertype(R),
has-value: (a)↓,
outr: outr(x),
outl: outl(x),
uimplies: b supposing a,
isinr: isinr def,
isinl: isinl def,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
pertype: pertype(R),
lambda: λx.A[x],
uimplies: b supposing a,
uand: uand(A;B),
has-value: (a)↓,
isinl: isinl def,
outl: outl(x),
isinr: isinr def,
equal: s = t ∈ T,
outr: outr(x),
per-void: per-void()
FDL editor aliases :
per-union
Latex:
per-union(A;B) ==
pertype(\mlambda{}a,b. uand(uand((a)\mdownarrow{};(b)\mdownarrow{});if a is inl then if b is inl then outl(a) = outl(b)
else per-void()
else if a is inr then if b is inr then outr(a) = outr(b)
else per-void()
else per-void()
supposing uand((a)\mdownarrow{};(b)\mdownarrow{})))
Date html generated:
2016_05_13-PM-03_54_49
Last ObjectModification:
2015_09_22-PM-05_45_34
Theory : per!type
Home
Index