---

Step * 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||. (F i) * p[i] = a ∈ ℚ
BY
{ ((RW (SweepDnC (HypC (-1))) 0) THENA 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 ∈ ℚ)
⊢ Σ0 ≤ i < ||p||. a * p[i] = a ∈ ℚ

---

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||.  (F  i)  *  p[i]  =  a


By

((RW  (SweepDnC  (HypC  (-1)))  0)  THENA  Auto)

---

Home Index