Nuprl Definition : per-partial
per-partial(T;x;y) ==  uiff((x)↓;(y)↓) ∧ x = y ∈ T supposing (x)↓
Definitions occuring in Statement : 
has-value: (a)↓
, 
uiff: uiff(P;Q)
, 
uimplies: b supposing a
, 
and: P ∧ Q
, 
equal: s = t ∈ T
Definitions occuring in definition : 
and: P ∧ Q
, 
uiff: uiff(P;Q)
, 
uimplies: b supposing a
, 
has-value: (a)↓
, 
equal: s = t ∈ T
FDL editor aliases : 
per-partial
Latex:
per-partial(T;x;y)  ==    uiff((x)\mdownarrow{};(y)\mdownarrow{})  \mwedge{}  x  =  y  supposing  (x)\mdownarrow{}
Date html generated:
2016_05_14-AM-06_09_20
Last ObjectModification:
2015_09_22-PM-05_46_14
Theory : partial_1
Home
Index