Nuprl Definition : compact-type
compact-type(T) == ∀p:T ⟶ 𝔹. ((∃x:T. p x = ff) ∨ (∀x:T. p x = tt))
Definitions occuring in Statement :
bfalse: ff,
btrue: tt,
bool: 𝔹,
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 :
function: x:A ⟶ B[x],
or: P ∨ Q,
exists: ∃x:A. B[x],
bfalse: ff,
all: ∀x:A. B[x],
equal: s = t ∈ T,
bool: 𝔹,
apply: f a,
btrue: tt
FDL editor aliases :
compact-type
Latex:
compact-type(T) == \mforall{}p:T {}\mrightarrow{} \mBbbB{}. ((\mexists{}x:T. p x = ff) \mvee{} (\mforall{}x:T. p x = tt))
Date html generated:
2016_05_15-PM-01_45_29
Last ObjectModification:
2015_09_23-AM-07_37_04
Theory : basic
Home
Index