Nuprl Definition : consistent-class
any x,y from X satisfy R[x; y] == ∀e1,e2:E. ∀v1,v2:T. (v1 ∈ X(e1) ⇒ v2 ∈ X(e2) ⇒ R[v1; v2])
Definitions occuring in Statement :
classrel: v ∈ X(e),
es-E: E,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
consistent-class
any x,y from X satisfy R[x; y] == \mforall{}e1,e2:E. \mforall{}v1,v2:T. (v1 \mmember{} X(e1) {}\mRightarrow{} v2 \mmember{} X(e2) {}\mRightarrow{} R[v1; v2])
Date html generated:
2015_07_17-PM-00_16_55
Last ObjectModification:
2012_02_25-PM-01_12_39
Home
Index