---

Step * of Lemma ireal-approx_functionality

∀[j:ℕ]. ∀[M:ℕ+]. ∀[z:ℤ]. ∀[x,y:ℝ].  j-approx(x;M;z) ⇐⇒ j-approx(y;M;z) supposing x = y
BY
{ (Auto THEN ParallelLast THEN (RWO "-2" (-1) ORELSE RWO "-2" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[j:\mBbbN{}].  \mforall{}[M:\mBbbN{}\msupplus{}].  \mforall{}[z:\mBbbZ{}].  \mforall{}[x,y:\mBbbR{}].    j-approx(x;M;z)  \mLeftarrow{}{}\mRightarrow{}  j-approx(y;M;z)  supposing  x  =  y


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  (RWO  "-2"  (-1)  ORELSE  RWO  "-2"  0)  THEN  Auto)

---

Home Index