Nuprl Definition : canonicalizable
canonicalizable(T) == ∃f:T ⟶ Base. ∀x:T. ((f x) = x ∈ T)
Definitions occuring in Statement :
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
base: Base,
all: ∀x:A. B[x],
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
canonicalizable
Latex:
canonicalizable(T) == \mexists{}f:T {}\mrightarrow{} Base. \mforall{}x:T. ((f x) = x)
Date html generated:
2016_05_13-PM-03_47_56
Last ObjectModification:
2015_09_22-PM-05_45_16
Theory : call!by!value_2
Home
Index