---

Step * of Lemma iter-arcsine-contraction_wf

∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[n:ℕ].  (arcsine-contraction^n(a) ∈ ℝ)
BY
{ (ProveWfLemma THEN (Assert λx.arcsine-contraction(a;x) ∈ ℝ ⟶ ℝ BY Auto) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}  ].  \mforall{}[n:\mBbbN{}].    (arcsine-contraction\^{}n(a)  \mmember{}  \mBbbR{})


By

---

Latex:
(ProveWfLemma  THEN  (Assert  \mlambda{}x.arcsine-contraction(a;x)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}  BY  Auto)  THEN  Auto)

---

Home Index