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