---

Step * 1 of Lemma q-linear-equal

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

---

Latex:

---

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


By

---

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

---

Home Index