Nuprl Definition : comem
comem{i:l}(x;s) == ∃t:set-dom(s). (x = set-item(s;t) ∈ coSet{i:l})
Definitions occuring in Statement :
set-item: set-item(s;x),
set-dom: set-dom(s),
coSet: coSet{i:l},
exists: ∃x:A. B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set-item: set-item(s;x),
coSet: coSet{i:l},
equal: s = t ∈ T,
set-dom: set-dom(s),
exists: ∃x:A. B[x]
FDL editor aliases :
comem
Latex:
comem\{i:l\}(x;s) == \mexists{}t:set-dom(s). (x = set-item(s;t))
Date html generated:
2018_07_29-AM-09_50_09
Last ObjectModification:
2018_07_11-PM-10_40_42
Theory : constructive!set!theory
Home
Index