---

Step * of Lemma int-int-retraction-reals

∃r:(ℤ ⟶ ℤ) ⟶ ℝ. ∀x:ℝ. (x = (r (λi.if i <z 1 then x 1 else x i fi )))
BY
{ ((Assert ∀x:ℝ. 2-regular-seq(x) BY
          (Auto THEN BLemma `real-regular` THEN Auto))
   THEN (InstLemma `int-int-retraction-reals-1` [⌜2⌝]⋅ THENA Auto)
   THEN (ParallelLast THENA Auto)
   THEN RWO "-1<" 0
   THEN Auto
   THEN BLemma `req-iff-bdd-diff`
   THEN Auto
   THEN RWO "accelerate-bdd-diff" 0
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mexists{}r:(\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbR{}.  \mforall{}x:\mBbbR{}.  (x  =  (r  (\mlambda{}i.if  i  <z  1  then  x  1  else  x  i  fi  )))


By

---

Latex:
((Assert  \mforall{}x:\mBbbR{}.  2-regular-seq(x)  BY
                (Auto  THEN  BLemma  `real-regular`  THEN  Auto))
  THEN  (InstLemma  `int-int-retraction-reals-1`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ParallelLast  THENA  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto
  THEN  BLemma  `req-iff-bdd-diff`
  THEN  Auto
  THEN  RWO  "accelerate-bdd-diff"  0
  THEN  EAuto  1)

---

Home Index