---

Step * of Lemma ws-monotone

∀[p:ℚ List]. ∀[F,G:ℕ||p|| ─→ ℚ].
  (weighted-sum(p;F) ≤ weighted-sum(p;G)) supposing ((∀x:ℕ||p||. ((F x) ≤ (G x))) and (∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))))
BY
{ (Auto THEN Repeat (MoveToConcl (-1))) }

1
∀p:ℚ List. ∀F,G:ℕ||p|| ─→ ℚ.
  ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))

---

Latex:


\mforall{}[p:\mBbbQ{}  List].  \mforall{}[F,G:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}].
    (weighted-sum(p;F)  \mleq{}  weighted-sum(p;G))  supposing 
          ((\mforall{}x:\mBbbN{}||p||.  ((F  x)  \mleq{}  (G  x)))  and 
          (\mforall{}q:\mBbbQ{}.  ((q  \mmember{}  p)  {}\mRightarrow{}  (0  \mleq{}  q))))


By

(Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index