Nuprl Definition : orderedpair-snds
snds(pr) == {x ∈ ⋃(pr) | seteq(pr;(fst(pr),x))}
Definitions occuring in Statement :
orderedpair-fst: fst(pr),
orderedpairset: (a,b),
unionset: ⋃(s),
sub-set: {a ∈ s | P[a]},
seteq: seteq(s1;s2)
Definitions occuring in definition :
orderedpair-fst: fst(pr),
orderedpairset: (a,b),
seteq: seteq(s1;s2),
unionset: ⋃(s),
sub-set: {a ∈ s | P[a]}
FDL editor aliases :
op-snds
Latex:
snds(pr) == \{x \mmember{} \mcup{}(pr) | seteq(pr;(fst(pr),x))\}
Date html generated:
2018_05_29-PM-01_49_02
Last ObjectModification:
2018_05_28-AM-10_07_26
Theory : constructive!set!theory
Home
Index