Nuprl Definition : rel-diamond-property
rel-diamond-property(T;x,y.R[x; y]) == ∀x,y,z:T. (R[x; y]
⇒ R[x; z]
⇒ ((y = z ∈ T) ∨ (∃w:T. (R[y; w] ∧ R[z; w]))))
Definitions occuring in Statement :
all: ∀x:A. B[x]
,
exists: ∃x:A. B[x]
,
implies: P
⇒ Q
,
or: P ∨ Q
,
and: P ∧ Q
,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
or: P ∨ Q
,
equal: s = t ∈ T
,
exists: ∃x:A. B[x]
,
and: P ∧ Q
FDL editor aliases :
rel-diamond-property
Latex:
rel-diamond-property(T;x,y.R[x; y]) ==
\mforall{}x,y,z:T. (R[x; y] {}\mRightarrow{} R[x; z] {}\mRightarrow{} ((y = z) \mvee{} (\mexists{}w:T. (R[y; w] \mwedge{} R[z; w]))))
Date html generated:
2019_10_15-AM-10_24_30
Last ObjectModification:
2019_08_16-PM-02_27_40
Theory : relations2
Home
Index