Nuprl Definition : set def
This primitive Nuprl type is essentially the same as ⌜Image((x:A × B[x]),(λp.(fst(p))))⌝
So its members are the members of A for which B[x] is true, but the evidence
for B[x] is not kept.
The elimination rule for this type is setElimination
From hypothesis u:{x:A| B[x]} we get u:A and a "hidden" B[u] that becomes
unhidden when we are proving a subgoal of the form equality or member. ⋅
{x:A| B[x]} == PRIMITIVE
Rules referencing :
setEquality,
dependent_set_memberFormation,
dependent_set_memberEquality,
setElimination,
strong_bar_Induction,
classicalIntroduction,
freeFromAtomSet
Latex:
\{x:A| B[x]\} == PRIMITIVE
Date html generated:
2017_09_29-PM-05_46_29
Last ObjectModification:
2017_09_22-AM-11_44_18
Theory : core_1
Home
Index