---

Step * 1 1 of Lemma ws-constant


1. a : ℚ
2. p : {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)} 
3. F : ℕ||p|| ⟶ ℚ
4. ∀x:ℕ||p||. ((F x) = a ∈ ℚ)
⊢ Σ0 ≤ i < ||p||. a * p[i] = a ∈ ℚ
BY
{ (RWO "prod_sum_l_q<" 0⋅ THEN Auto') }

1
1. a : ℚ
2. p : {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)} 
3. F : ℕ||p|| ⟶ ℚ
4. ∀x:ℕ||p||. ((F x) = a ∈ ℚ)
⊢ (a * Σ0 ≤ i < ||p||. p[i]) = a ∈ ℚ

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  p  :  \{p:\mBbbQ{}  List|  (\mSigma{}0  \mleq{}  i  <  ||p||.  p[i]  =  1)  \mwedge{}  (\mforall{}q\mmember{}p.0  \mleq{}  q)\} 
3.  F  :  \mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}
4.  \mforall{}x:\mBbbN{}||p||.  ((F  x)  =  a)
\mvdash{}  \mSigma{}0  \mleq{}  i  <  ||p||.  a  *  p[i]  =  a


By

---

Latex:
(RWO  "prod\_sum\_l\_q<"  0\mcdot{}  THEN  Auto')

---

Home Index