---

Step * 1 of Lemma sq_stable_double_ex_rneq


1. m : ℕ
2. n : ℕ
3. a : ℕm ⟶ ℕn ⟶ ℝ
4. b : ℕm ⟶ ℕn ⟶ ℝ
5. ↓∃i:ℕm. (r0 < Σ{|a[i;j] - b[i;j]| | 0≤j≤n - 1})
6. r0 < Σ{Σ{|a[i;j] - b[i;j]| | 0≤j≤n - 1} | 0≤i≤m - 1} ⇐⇒ ∃i:ℕm. (r0 < Σ{|a[i;j] - b[i;j]| | 0≤j≤n - 1})
⊢ ∃i:ℕm. (r0 < Σ{|a[i;j] - b[i;j]| | 0≤j≤n - 1})
BY
{ ((RWO "-1<" 0 THENA Auto) THEN (RWO "-1<" (-2) THENA Auto) THEN D -2 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  a  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
4.  b  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
5.  \mdownarrow{}\mexists{}i:\mBbbN{}m.  (r0  <  \mSigma{}\{|a[i;j]  -  b[i;j]|  |  0\mleq{}j\mleq{}n  -  1\})
6.  r0  <  \mSigma{}\{\mSigma{}\{|a[i;j]  -  b[i;j]|  |  0\mleq{}j\mleq{}n  -  1\}  |  0\mleq{}i\mleq{}m  -  1\}
\mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}m.  (r0  <  \mSigma{}\{|a[i;j]  -  b[i;j]|  |  0\mleq{}j\mleq{}n  -  1\})
\mvdash{}  \mexists{}i:\mBbbN{}m.  (r0  <  \mSigma{}\{|a[i;j]  -  b[i;j]|  |  0\mleq{}j\mleq{}n  -  1\})


By

---

Latex:
((RWO  "-1<"  0  THENA  Auto)  THEN  (RWO  "-1<"  (-2)  THENA  Auto)  THEN  D  -2  THEN  Unhide  THEN  Auto)

---

Home Index