Nuprl Definition : homeo-image
homeo-image(A;Y;dY;h) == {y:Y| ∃a:A. y ≡ (fst(h)) a}
Definitions occuring in Statement :
meq: x ≡ y,
pi1: fst(t),
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
apply: f a
FDL editor aliases :
homeo-image
Latex:
homeo-image(A;Y;dY;h) == \{y:Y| \mexists{}a:A. y \mequiv{} (fst(h)) a\}
Date html generated:
2020_05_20-AM-11_50_25
Last ObjectModification:
2019_11_07-PM-01_46_48
Theory : reals
Home
Index