Nuprl Definition : p-selector

is "root" of the decidable property p
if ff  
(thinking of ff as being and tt as non-zero).

is selector for decidable property if
is root of if and only if has root.
non-void, compact type has selector
  see: compact-type-compact-type2)⋅

p-selector(T;x;p) ==  (∃y:T. ff)  ff

Definitions occuring in Statement :  bfalse: ff bool: 𝔹 exists: x:A. B[x] implies:  Q apply: a equal: t ∈ T
Definitions occuring in definition :  implies:  Q exists: x:A. B[x] equal: t ∈ T bool: 𝔹 apply: a bfalse: ff
FDL editor aliases :  p-selector

p-selector(T;x;p)  ==    (\mexists{}y:T.  p  y  =  ff)  {}\mRightarrow{}  p  x  =  ff

Date html generated: 2016_07_08-PM-04_55_02
Last ObjectModification: 2015_09_23-AM-07_37_04

Theory : basic

Home Index