---

Step * 2 of Lemma q-linear-equal

.....upcase..... 
1. k : ℤ
2. 0 < k
3. ∀[X:ℕ ⟶ ℚ]. ∀[y,z:ℚ List].
     (q-linear(k - 1;j.X[j];y) = q-linear(k - 1;j.X[j];z) ∈ ℚ) supposing 
        ((∀i:ℕk - 1. (y[i] = z[i] ∈ ℚ)) and 
        ((k - 1) ≤ ||z||) and 
        ((k - 1) ≤ ||y||))
⊢ ∀[X:ℕ ⟶ ℚ]. ∀[y,z:ℚ List].
    (q-linear(k;j.X[j];y) = q-linear(k;j.X[j];z) ∈ ℚ) supposing 
       ((∀i:ℕk. (y[i] = z[i] ∈ ℚ)) and 
       (k ≤ ||z||) and 
       (k ≤ ||y||))
BY
{ TACTIC:((Auto THEN RWO "q-linear-unroll" 0 THEN Auto) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:
.....upcase..... 
1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[y,z:\mBbbQ{}  List].
          (q-linear(k  -  1;j.X[j];y)  =  q-linear(k  -  1;j.X[j];z))  supposing 
                ((\mforall{}i:\mBbbN{}k  -  1.  (y[i]  =  z[i]))  and 
                ((k  -  1)  \mleq{}  ||z||)  and 
                ((k  -  1)  \mleq{}  ||y||))
\mvdash{}  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[y,z:\mBbbQ{}  List].
        (q-linear(k;j.X[j];y)  =  q-linear(k;j.X[j];z))  supposing 
              ((\mforall{}i:\mBbbN{}k.  (y[i]  =  z[i]))  and 
              (k  \mleq{}  ||z||)  and 
              (k  \mleq{}  ||y||))


By

---

Latex:
TACTIC:((Auto  THEN  RWO  "q-linear-unroll"  0  THEN  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index