---

Step * of Lemma rsin_wf1

∀[x:ℝ]. (rsin(x) ∈ {y:ℝ| sine(x) = y} )
BY
{ (Auto
   THEN (InstLemma `approx-arg_wf` [⌜λ2x.sine(x)⌝;⌜λ2x.cosine(x)⌝;⌜1⌝;⌜x⌝]⋅ THENA Auto)
   THEN Unfold `so_lambda` -1
   THEN Fold
   `rsin` (-1)⋅) }

1
1. x : ℝ
2. rsin(x) ∈ {y:ℝ| y = sine(x)} 
⊢ rsin(x) ∈ {y:ℝ| sine(x) = y} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rsin(x)  \mmember{}  \{y:\mBbbR{}|  sine(x)  =  y\}  )


By

---

Latex:
(Auto
  THEN  (InstLemma  `approx-arg\_wf`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.sine(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.cosine(x)\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `so\_lambda`  -1
  THEN  Fold
  `rsin`  (-1)\mcdot{})

---

Home Index