---

Step * of Lemma sq_stable_double_ex_rneq

∀m,n:ℕ. ∀a,b:ℕm ⟶ ℕn ⟶ ℝ.  SqStable(∃i:ℕm. ∃j:ℕn. a[i;j] ≠ b[i;j])
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (All (RWW "exists-rneq-iff") THENA Auto)
   THEN (InstLemma `rsum-of-nonneg-positive-iff` [⌜0⌝;⌜m - 1⌝;⌜λ2i.Σ{|a[i;j] - b[i;j]| | 0≤j≤n - 1}⌝]⋅
         THENA (Auto THEN BLemma `rsum_nonneg` THEN Auto THEN D 0 THEN Auto)
         )
   THEN (Subst' (m - 1) + 1 ~ m -1 THENA Auto)) }

1
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})

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (All  (RWW  "exists-rneq-iff")  THENA  Auto)
  THEN  (InstLemma  `rsum-of-nonneg-positive-iff`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}m  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.\mSigma{}\{|a[i;j]  -  b[i;j]|  |  0\mleq{}j\mleq{}n  -  1\}\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `rsum\_nonneg`  THEN  Auto  THEN  D  0  THEN  Auto)
              )
  THEN  (Subst'  (m  -  1)  +  1  \msim{}  m  -1  THENA  Auto))

---

Home Index