---

Step * of Lemma sq_stable_ex_rneq

∀n:ℕ. ∀a,b:ℕn ⟶ ℝ.  SqStable(∃i:ℕn. a[i] ≠ b[i])
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. n : ℕ
2. a : ℕn ⟶ ℝ
3. b : ℕn ⟶ ℝ
4. ↓∃i:ℕn. a[i] ≠ b[i]
⊢ ∃i:ℕn. a[i] ≠ b[i]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.    SqStable(\mexists{}i:\mBbbN{}n.  a[i]  \mneq{}  b[i])


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index