Nuprl Definition : imageset
imageset(B;f) == {b ∈ B | ∃pr∈f.seteq(b;snd(pr))}
Definitions occuring in Statement :
orderedpair-snd: snd(pr),
existssetmem: ∃a∈A.P[a],
sub-set: {a ∈ s | P[a]},
seteq: seteq(s1;s2)
Definitions occuring in definition :
orderedpair-snd: snd(pr),
seteq: seteq(s1;s2),
existssetmem: ∃a∈A.P[a],
sub-set: {a ∈ s | P[a]}
FDL editor aliases :
imageset
Latex:
imageset(B;f) == \{b \mmember{} B | \mexists{}pr\mmember{}f.seteq(b;snd(pr))\}
Date html generated:
2018_05_29-PM-01_51_12
Last ObjectModification:
2018_05_28-AM-11_26_23
Theory : constructive!set!theory
Home
Index