---

Step * of Lemma blended-real_wf

∀[k:ℕ+]. ∀[x,y:ℝ].  blended-real(k;x;y) ∈ ℝ supposing |x - y| ≤ (r1/r(k))
BY
{ (ProveWfLemma THEN MemTypeCD THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x,y:\mBbbR{}].    blended-real(k;x;y)  \mmember{}  \mBbbR{}  supposing  |x  -  y|  \mleq{}  (r1/r(k))


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  EAuto  1)

---

Home Index