Nuprl Lemma : sine-small_wf
∀[x:{x:ℝ| |x| ≤ (r1/r(2))} ]. (sine-small(x) ∈ {y:ℝ| y = sine(x)} )
Proof
Error : references
Latex:
\mforall{}[x:\{x:\mBbbR{}| |x| \mleq{} (r1/r(2))\} ]. (sine-small(x) \mmember{} \{y:\mBbbR{}| y = sine(x)\} )
Date html generated:
2020_05_21-AM-10_27_23
Last ObjectModification:
2019_02_02-AM-10_37_31
Theory : reals
Home
Index