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