Nuprl Definition : m-retraction
Retract(X ⟶ A) ==  {f:X ⟶ A| f:FUN(X;A) ∧ (∀a:A. f a ≡ a)} 
Definitions occuring in Statement : 
is-mfun: f:FUN(X;Y)
, 
meq: x ≡ y
, 
all: ∀x:A. B[x]
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
function: x:A ⟶ B[x]
FDL editor aliases : 
m-retraction
Latex:
Retract(X  {}\mrightarrow{}  A)  ==    \{f:X  {}\mrightarrow{}  A|  f:FUN(X;A)  \mwedge{}  (\mforall{}a:A.  f  a  \mequiv{}  a)\} 
Date html generated:
2020_05_20-AM-11_48_46
Last ObjectModification:
2019_11_11-PM-02_18_54
Theory : reals
Home
Index