Nuprl Definition : compact-type2

compact-type2(T) ==  ∀p:T ⟶ 𝔹(∃x:{T| p-selector(T;x;p)})



Definitions occuring in Statement :  p-selector: p-selector(T;x;p) bool: 𝔹 all: x:A. B[x] sq_exists: x:{A| B[x]} function: x:A ⟶ B[x]
Definitions occuring in definition :  all: x:A. B[x] function: x:A ⟶ B[x] bool: 𝔹 sq_exists: x:{A| B[x]} p-selector: p-selector(T;x;p)
FDL editor aliases :  compact-type2

Latex:
compact-type2(T)  ==    \mforall{}p:T  {}\mrightarrow{}  \mBbbB{}.  (\mexists{}x:\{T|  p-selector(T;x;p)\})



Date html generated: 2016_05_15-PM-01_45_35
Last ObjectModification: 2015_09_23-AM-07_37_05

Theory : basic


Home Index