Nuprl Definition : tunion_def
The union of a family types B[x], x ∈ A is obtained from the type
x:A × B[x] of all pairs <a, b>, a ∈ A, b ∈ B[a] by projection onto the
second component. That means that b ∈ ⋃x:A.B[x] if for some a ∈ A,
<a, b> ∈ x:A × B[x].⋅
⋃x:A.B[x] == Image((x:A × B[x]),(λp.(snd(p))))
Definitions occuring in Statement :
pi2: snd(t),
image-type: Image(T,f),
lambda: λx.A[x],
product: x:A × B[x]
Definitions occuring in definition :
image-type: Image(T,f),
product: x:A × B[x],
lambda: λx.A[x],
pi2: snd(t)
Latex:
\mcup{}x:A.B[x] == Image((x:A \mtimes{} B[x]),(\mlambda{}p.(snd(p))))
Date html generated:
2016_07_08-PM-04_46_30
Last ObjectModification:
2016_01_04-AM-10_24_05
Theory : core_2
Home
Index