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