Nuprl Definition : set-eq
set-eq(s;s') ==
νR.λs,s'. ((∀i:set-dom(s). ∃j:set-dom(s'). (R set-item(s;i) set-item(s';j)))
∧ (∀j:set-dom(s'). ∃i:set-dom(s). (R set-item(s;i) set-item(s';j))))
s
s'
Definitions occuring in Statement :
set-item: set-item(s;x),
set-dom: set-dom(s),
bigrel: νR.F[R],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
bigrel: νR.F[R],
lambda: λx.A[x],
and: P ∧ Q,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
set-dom: set-dom(s),
apply: f a,
set-item: set-item(s;x)
FDL editor aliases :
set-eq
Latex:
set-eq(s;s') ==
\mnu{}R.\mlambda{}s,s'. ((\mforall{}i:set-dom(s). \mexists{}j:set-dom(s'). (R set-item(s;i) set-item(s';j)))
\mwedge{} (\mforall{}j:set-dom(s'). \mexists{}i:set-dom(s). (R set-item(s;i) set-item(s';j))))
s
s'
Date html generated:
2019_10_31-AM-06_32_42
Last ObjectModification:
2018_08_04-PM-05_16_23
Theory : constructive!set!theory
Home
Index