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