---

Step * of Lemma reals-complete-ext

No Annotations
mcomplete(ℝ with rmetric())
BY
{ Extract of Obid: reals-complete
  not unfolding  divide
  finishing with Auto
  normalizes to:
  
  λx,%. <λn.eval m = 4 * n in (x (% m) m) ÷ 4, λk.((% (4 * k)) + 1)> }

---

Latex:

---

Latex:
No  Annotations
mcomplete(\mBbbR{}  with  rmetric())


By

---

Latex:
Extract  of  Obid:  reals-complete
not  unfolding    divide
finishing  with  Auto
normalizes  to:

\mlambda{}x,\%.  <\mlambda{}n.eval  m  =  4  *  n  in  (x  (\%  m)  m)  \mdiv{}  4,  \mlambda{}k.((\%  (4  *  k))  +  1)>

---

Home Index