---

Step * of Lemma arcsine0

arcsine(r0) = r0
BY
{ (Unfold `arcsine` 0 THEN Using [`I', ⌜(r(-1), r1)⌝ ] (BLemma `integral-same-endpoints`)⋅ THEN Auto) }

1
λt.arcsine_deriv(t) ∈ {f:(r(-1), r1) ⟶ℝ| ∀x,y:{a:ℝ| (r(-1) < a) ∧ (a < r1)} .  ((x = y) ⇒ ((f x) = (f y)))} 

---

Latex:

---

Latex:
arcsine(r0)  =  r0


By

---

Latex:
(Unfold  `arcsine`  0  THEN  Using  [`I',  \mkleeneopen{}(r(-1),  r1)\mkleeneclose{}  ]  (BLemma  `integral-same-endpoints`)\mcdot{}  THEN  Auto)

---

Home Index