Nuprl Definition : rv-T'
rv-T'(n;a;b;c) == ∀x,y:ℝ^n. (x-a-y ⇒ x-c-y ⇒ x-b-y)
Definitions occuring in Statement :
rv-between: a-b-c,
real-vec: ℝ^n,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
rv-between: a-b-c,
implies: P ⇒ Q,
real-vec: ℝ^n,
all: ∀x:A. B[x]
FDL editor aliases :
rv-T'
Latex:
rv-T'(n;a;b;c) == \mforall{}x,y:\mBbbR{}\^{}n. (x-a-y {}\mRightarrow{} x-c-y {}\mRightarrow{} x-b-y)
Date html generated:
2016_10_26-AM-10_50_54
Last ObjectModification:
2016_10_06-PM-01_17_01
Theory : reals
Home
Index