---

Step * of Lemma arcsine-contraction_wf

∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x:ℝ].  (arcsine-contraction(a;x) ∈ ℝ)
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN nRAdd  ⌜a * a⌝ 0⋅
   THEN RWW  "rnexp2< square-rleq-1-iff rabs-rleq-iff" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  nRAdd    \mkleeneopen{}a  *  a\mkleeneclose{}  0\mcdot{}
  THEN  RWW    "rnexp2<  square-rleq-1-iff  rabs-rleq-iff"  0
  THEN  Auto)

---

Home Index