Nuprl Definition : decidable-non-minimal
decidable-non-minimal(T;x,y.R[x; y]) == ∀y:T. Dec(↓∃x:T. R[x; y])
Definitions occuring in Statement :
decidable: Dec(P),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T
Definitions occuring in definition :
all: ∀x:A. B[x],
decidable: Dec(P),
squash: ↓T,
exists: ∃x:A. B[x]
FDL editor aliases :
decidable-non-minimal
Latex:
decidable-non-minimal(T;x,y.R[x; y]) == \mforall{}y:T. Dec(\mdownarrow{}\mexists{}x:T. R[x; y])
Date html generated:
2016_05_15-PM-07_50_53
Last ObjectModification:
2015_09_23-AM-08_19_09
Theory : general
Home
Index