Nuprl Definition : retractible
retractible(T) == ∃f:Base. ((∀x:T. ((f x) = x ∈ T)) ∧ (∀x:Base. ((f x)↓ ⇒ (x ∈ T))))
Definitions occuring in Statement :
has-value: (a)↓,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
apply: f a,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
all: ∀x:A. B[x],
base: Base,
implies: P ⇒ Q,
has-value: (a)↓,
apply: f a,
member: t ∈ T
FDL editor aliases :
retractible
Latex:
retractible(T) == \mexists{}f:Base. ((\mforall{}x:T. ((f x) = x)) \mwedge{} (\mforall{}x:Base. ((f x)\mdownarrow{} {}\mRightarrow{} (x \mmember{} T))))
Date html generated:
2016_05_13-PM-03_48_12
Last ObjectModification:
2015_09_22-PM-05_45_17
Theory : call!by!value_2
Home
Index