---

Step * of Lemma reals-close-or-rneq-ext

No Annotations
∀K:ℕ+
  (∃g:ℝ ⟶ ℝ ⟶ ℕ3 [(∀x,y:ℝ.
                       ((((g x y) = 1 ∈ ℤ) ⇒ ((r1/r(K)) < (y - x)))
                       ∧ (((g x y) = 2 ∈ ℤ) ⇒ ((r1/r(K)) < (x - y)))
                       ∧ (((g x y) = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(K))))))])
BY
{ Extract of Obid: reals-close-or-rneq
  not unfolding  absval rsub int-rdiv int-to-real
  finishing with (Unfold `rclose-or-sep` 0 THEN RepeatFor 5 (EqCD) THEN Try (RWO "mul-associates<" 0) THEN Auto)
  normalizes to:
  
  λK,x,y. rclose-or-sep(K;x;y) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}K:\mBbbN{}\msupplus{}
    (\mexists{}g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbN{}3  [(\mforall{}x,y:\mBbbR{}.
                                              ((((g  x  y)  =  1)  {}\mRightarrow{}  ((r1/r(K))  <  (y  -  x)))
                                              \mwedge{}  (((g  x  y)  =  2)  {}\mRightarrow{}  ((r1/r(K))  <  (x  -  y)))
                                              \mwedge{}  (((g  x  y)  =  0)  {}\mRightarrow{}  (|x  -  y|  <  (r(2)/r(K))))))])


By

---

Latex:
Extract  of  Obid:  reals-close-or-rneq
not  unfolding    absval  rsub  int-rdiv  int-to-real
finishing  with  (Unfold  `rclose-or-sep`  0
                                THEN  RepeatFor  5  (EqCD)
                                THEN  Try  (RWO  "mul-associates<"  0)
                                THEN  Auto)
normalizes  to:

\mlambda{}K,x,y.  rclose-or-sep(K;x;y)

---

Home Index