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