Nuprl Definition : retraction
retraction(T;f) == ∃h:T ⟶ ℕ. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
all: ∀x:A. B[x],
or: P ∨ Q,
equal: s = t ∈ T,
less_than: a < b,
apply: f a
FDL editor aliases :
retraction
Latex:
retraction(T;f) == \mexists{}h:T {}\mrightarrow{} \mBbbN{}. \mforall{}x:T. (((f x) = x) \mvee{} h (f x) < h x)
Date html generated:
2016_05_15-PM-05_05_22
Last ObjectModification:
2015_09_23-AM-07_51_19
Theory : general
Home
Index