Nuprl Definition : allsetmem
∀a∈A.P[a] == ∀i:set-dom(A). P[set-item(A;i)]
Definitions occuring in Statement :
set-item: set-item(s;x),
set-dom: set-dom(s),
all: ∀x:A. B[x]
Definitions occuring in definition :
set-item: set-item(s;x),
set-dom: set-dom(s),
all: ∀x:A. B[x]
FDL editor aliases :
allsetmem
Latex:
\mforall{}a\mmember{}A.P[a] == \mforall{}i:set-dom(A). P[set-item(A;i)]
Date html generated:
2018_05_29-PM-01_48_13
Last ObjectModification:
2018_05_26-PM-07_30_31
Theory : constructive!set!theory
Home
Index