---

Step * 1 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 ∈ ℚ)
⊢ (a * Σ0 ≤ i < ||p||. p[i]) = a ∈ ℚ
BY
{ ((D -3 THEN ExRepD) THEN HypSubst' -4 0 THEN Auto)⋅ }

---

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{}  (a  *  \mSigma{}0  \mleq{}  i  <  ||p||.  p[i])  =  a


By

---

Latex:
((D  -3  THEN  ExRepD)  THEN  HypSubst'  -4  0  THEN  Auto)\mcdot{}

---

Home Index