---

Step * 1 3 of Lemma ws-monotone


1. ∀d:ℕ. ∀p:ℚ List.
     ((||p|| ≤ d)
     ⇒ (∀F,G:ℕ||p|| ─→ ℚ.
           ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))
2. p : ℚ List@i
3. F : ℕ||p|| ─→ ℚ@i
4. G : ℕ||p|| ─→ ℚ@i
5. ∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))@i
6. ∀x:ℕ||p||. ((F x) ≤ (G x))@i
7. ∀F,G:ℕ||p|| ─→ ℚ.
     ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))
⊢ weighted-sum(p;F) ≤ weighted-sum(p;G)
BY
{ (BHyp -1  THEN Auto) }

---

Latex:



1.  \mforall{}d:\mBbbN{}.  \mforall{}p:\mBbbQ{}  List.
          ((||p||  \mleq{}  d)
          {}\mRightarrow{}  (\mforall{}F,G:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}.
                      ((\mforall{}q:\mBbbQ{}.  ((q  \mmember{}  p)  {}\mRightarrow{}  (0  \mleq{}  q)))
                      {}\mRightarrow{}  (\mforall{}x:\mBbbN{}||p||.  ((F  x)  \mleq{}  (G  x)))
                      {}\mRightarrow{}  (weighted-sum(p;F)  \mleq{}  weighted-sum(p;G)))))
2.  p  :  \mBbbQ{}  List@i
3.  F  :  \mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}@i
4.  G  :  \mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}@i
5.  \mforall{}q:\mBbbQ{}.  ((q  \mmember{}  p)  {}\mRightarrow{}  (0  \mleq{}  q))@i
6.  \mforall{}x:\mBbbN{}||p||.  ((F  x)  \mleq{}  (G  x))@i
7.  \mforall{}F,G:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}.
          ((\mforall{}q:\mBbbQ{}.  ((q  \mmember{}  p)  {}\mRightarrow{}  (0  \mleq{}  q)))
          {}\mRightarrow{}  (\mforall{}x:\mBbbN{}||p||.  ((F  x)  \mleq{}  (G  x)))
          {}\mRightarrow{}  (weighted-sum(p;F)  \mleq{}  weighted-sum(p;G)))
\mvdash{}  weighted-sum(p;F)  \mleq{}  weighted-sum(p;G)


By

(BHyp  -1    THEN  Auto)

---

Home Index