---

Step * of Lemma blended-real-req

∀[k:ℕ+]. ∀[x,y:ℝ].  blended-real(k;x;y) = y supposing |x - y| ≤ (r1/r(k))
BY
{ (Auto
   THEN (Assert ∀z:ℝ. 3-regular-seq(z) BY
               (Auto THEN BLemma `real-regular` THEN Auto))
   THEN Assert ⌜(blended-real(k;x;y) = accelerate(3;y)) ∧ (accelerate(3;y) = y)⌝⋅
   THEN Auto
   THEN BLemma `req-iff-bdd-diff`
   THEN Auto) }

1
1. k : ℕ+
2. x : ℝ
3. y : ℝ
4. |x - y| ≤ (r1/r(k))
5. ∀z:ℝ. 3-regular-seq(z)
⊢ bdd-diff(blended-real(k;x;y);accelerate(3;y))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}z:\mBbbR{}.  3-regular-seq(z)  BY
                          (Auto  THEN  BLemma  `real-regular`  THEN  Auto))
  THEN  Assert  \mkleeneopen{}(blended-real(k;x;y)  =  accelerate(3;y))  \mwedge{}  (accelerate(3;y)  =  y)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BLemma  `req-iff-bdd-diff`
  THEN  Auto)

---

Home Index