---

Step * 1 1 2 1 1 1 of Lemma 0-dim-complex-polyhedron


1. k : ℕ
2. u : ℕk ⟶ ℚ
3. a : ℕk ⟶ ℚ
⊢ (¬(u = a ∈ (ℕk ⟶ ℚ))) ⇒ λj.rat2real(u j) ≠ λj.rat2real(a j)
BY
{ ((RWO "real-vec-sep-iff-rneq" 0 THENA Auto) THEN Reduce 0 THEN (RWO  "rneq-rat2real" 0 THENA Auto)) }

1
1. k : ℕ
2. u : ℕk ⟶ ℚ
3. a : ℕk ⟶ ℚ
⊢ (¬(u = a ∈ (ℕk ⟶ ℚ))) ⇒ (∃i:ℕk. (¬((u i) = (a i) ∈ ℚ)))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  u  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
3.  a  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
\mvdash{}  (\mneg{}(u  =  a))  {}\mRightarrow{}  \mlambda{}j.rat2real(u  j)  \mneq{}  \mlambda{}j.rat2real(a  j)


By

---

Latex:
((RWO  "real-vec-sep-iff-rneq"  0  THENA  Auto)  THEN  Reduce  0  THEN  (RWO    "rneq-rat2real"  0  THENA  Auto))

---

Home Index