Nuprl Definition : rv-T
rv-T(n;a;b;c) == (a ≠ c ⇒ real-vec-be(n;a;b;c)) ∧ ((¬a ≠ c) ⇒ (¬b ≠ c))
Definitions occuring in Statement :
real-vec-sep: a ≠ b,
real-vec-be: real-vec-be(n;a;b;c),
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
real-vec-sep: a ≠ b,
not: ¬A,
implies: P ⇒ Q,
real-vec-be: real-vec-be(n;a;b;c),
and: P ∧ Q
FDL editor aliases :
rv-T
Latex:
rv-T(n;a;b;c) == (a \mneq{} c {}\mRightarrow{} real-vec-be(n;a;b;c)) \mwedge{} ((\mneg{}a \mneq{} c) {}\mRightarrow{} (\mneg{}b \mneq{} c))
Date html generated:
2016_10_26-AM-10_45_22
Last ObjectModification:
2016_10_05-PM-00_01_32
Theory : reals
Home
Index