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
{ xxx(Auto THEN Repeat (MoveToConcl (-1)))xxx }
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:
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
Latex:
xxx(Auto THEN Repeat (MoveToConcl (-1)))xxx
Home
Index