---

Step * of Lemma near-arcsine_wf

∀a:{a:ℝ| a ∈ (r(-1), r1)} . ∀N:ℕ+.  (near-arcsine(a;N) ∈ {y:ℝ| |y - arcsine(a)| ≤ (r1/r(N))} )
BY
{ (Auto
   THEN Fold `sq_exists` 0
   THEN Subst' near-arcsine(a;N) ~ TERMOF{near-arcsine-exists-ext:o, 1:l} a N 0
   THEN Auto) }

1
.....equality..... 
1. a : {a:ℝ| a ∈ (r(-1), r1)} 
2. N : ℕ+
⊢ near-arcsine(a;N) ~ TERMOF{near-arcsine-exists-ext:o, 1:l} a N

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  (r(-1),  r1)\}  .  \mforall{}N:\mBbbN{}\msupplus{}.    (near-arcsine(a;N)  \mmember{}  \{y:\mBbbR{}|  |y  -  arcsine(a)|  \mleq{}  (r1/r(N))\}  )


By

---

Latex:
(Auto
  THEN  Fold  `sq\_exists`  0
  THEN  Subst'  near-arcsine(a;N)  \msim{}  TERMOF\{near-arcsine-exists-ext:o,  1:l\}  a  N  0
  THEN  Auto)

---

Home Index