Nuprl Lemma : real-vec-be-unique-1

∀[n:ℕ]. ∀[x,y,u,v:ℝ^n].
  ((||x|| ≤ r1)
  ⇒ (||y|| ≤ r1)
  ⇒ x ≠ y
  ⇒ (||v|| = r1)
  ⇒ (||u|| = r1)
  ⇒ real-vec-be(n;u;x;y)
  ⇒ real-vec-be(n;v;x;y)
  ⇒ req-vec(n;u;v))
Error : references

Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[x,y,u,v:\mBbbR{}\^{}n]. ((||x|| \mleq{} r1) {}\mRightarrow{} (||y|| \mleq{} r1) {}\mRightarrow{} x \mneq{} y {}\mRightarrow{} (||v|| = r1) {}\mRightarrow{} (||u|| = r1) {}\mRightarrow{} real-vec-be(n;u;x;y) {}\mRightarrow{} real-vec-be(n;v;x;y) {}\mRightarrow{} req-vec(n;u;v)) Date html generated: 2019_11_06-PM-00_35_50 Last ObjectModification: 2019_07_09-AM-10_46_59 Theory : real!vectors Home Index