---

Step * 1 of Lemma arcsine0


λt.arcsine_deriv(t) ∈ {f:(r(-1), r1) ⟶ℝ| ∀x,y:{a:ℝ| (r(-1) < a) ∧ (a < r1)} .  ((x = y) ⇒ ((f x) = (f y)))} 
BY
{ ((MemTypeCD THEN Reduce 0 THEN Auto) THEN RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

\mlambda{}t.arcsine\_deriv(t)  \mmember{}  \{f:(r(-1),  r1)  {}\mrightarrow{}\mBbbR{}| 
                                              \mforall{}x,y:\{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\} 


By

---

Latex:
((MemTypeCD  THEN  Reduce  0  THEN  Auto)  THEN  RWO    "-1"  0  THEN  Auto)

---

Home Index