Nuprl Definition : name-morph-range
name-morph-range(f;I) == {x:Cname| ∃i:nameset(I). ((↑isname(f i)) ∧ ((f i) = x ∈ Cname))}
Definitions occuring in Statement :
isname: isname(z),
nameset: nameset(L),
coordinate_name: Cname,
assert: ↑b,
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
exists: ∃x:A. B[x],
nameset: nameset(L),
and: P ∧ Q,
assert: ↑b,
isname: isname(z),
equal: s = t ∈ T,
coordinate_name: Cname,
apply: f a
FDL editor aliases :
name-morph-range
Latex:
name-morph-range(f;I) == \{x:Cname| \mexists{}i:nameset(I). ((\muparrow{}isname(f i)) \mwedge{} ((f i) = x))\}
Date html generated:
2016_05_20-AM-09_30_35
Last ObjectModification:
2015_09_23-AM-09_29_31
Theory : cubical!sets
Home
Index