---

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


1. k : ℕ
2. u : ℕk ⟶ ℚ
3. a : ℕk ⟶ ℚ
⊢ (¬(u = a ∈ (ℕk ⟶ ℚ))) ⇒ (∃i:ℕk. (¬((u i) = (a i) ∈ ℚ)))
BY
{ (NatInd 1 THEN Auto) }

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

2
1. k : ℤ
2. [%1] : 0 < k
3. ∀u,a:ℕk - 1 ⟶ ℚ.  ((¬(u = a ∈ (ℕk - 1 ⟶ ℚ))) ⇒ (∃i:ℕk - 1. (¬((u i) = (a i) ∈ ℚ))))
4. u : ℕk ⟶ ℚ
5. a : ℕk ⟶ ℚ
6. ¬(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{}  (\mexists{}i:\mBbbN{}k.  (\mneg{}((u  i)  =  (a  i))))


By

---

Latex:
(NatInd  1  THEN  Auto)

---

Home Index