---

Step * of Lemma q-linear-equal

∀[k:ℕ]. ∀[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:InductionOnNat }

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

2
.....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||))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \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:InductionOnNat

---

Home Index