---

Step * of Lemma quasilinear-weighted-mean_wf

∀[I,J:Interval]. ∀[f:{x:ℝ| x ∈ J}  ⟶ {x:ℝ| x ∈ I} ]. ∀[g:{x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ J} ].
  (quasilinear-weighted-mean(f;g) ∈ {x:ℝ| x ∈ I} 
   ⟶ {x:ℝ| x ∈ I} 
   ⟶ r:{r:ℝ| r0 ≤ r} 
   ⟶ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} 
   ⟶ {x:ℝ| x ∈ I} )
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[I,J:Interval].  \mforall{}[f:\{x:\mBbbR{}|  x  \mmember{}  J\}    {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  ].  \mforall{}[g:\{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  J\}  ].
    (quasilinear-weighted-mean(f;g)  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 
      {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 
      {}\mrightarrow{}  r:\{r:\mBbbR{}|  r0  \mleq{}  r\} 
      {}\mrightarrow{}  \{s:\mBbbR{}|  (r0  \mleq{}  s)  \mwedge{}  (r0  <  (r  +  s))\} 
      {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  )


By

---

Latex:
ProveWfLemma

---

Home Index