Nuprl Definition : image-space

f[X] ==  y:Y × {x:X| y ≡ x} 



Definitions occuring in Statement :  meq: x ≡ y set: {x:A| B[x]}  apply: a product: x:A × B[x]
Definitions occuring in definition :  apply: a meq: x ≡ y set: {x:A| B[x]}  product: x:A × B[x]
FDL editor aliases :  image-space image-space

Latex:
f[X]  ==    y:Y  \mtimes{}  \{x:X|  y  \mequiv{}  f  x\} 



Date html generated: 2019_10_30-AM-06_33_49
Last ObjectModification: 2019_10_25-AM-11_14_07

Theory : reals


Home Index