Step
*
1
1
of Lemma
arctangent_functionality_wrt_rless
.....antecedent..... 
1. ∀x:ℝ. (r0 < (r1 + x^2))
2. x : ℝ
3. y : ℝ
4. [%] : x < y
⊢ (r1/r1 + x^2) continuous for x ∈ (-∞, ∞)
BY
{ (BLemma `function-is-continuous` THEN Auto) }
Latex:
Latex:
.....antecedent..... 
1.  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))
2.  x  :  \mBbbR{}
3.  y  :  \mBbbR{}
4.  [\%]  :  x  <  y
\mvdash{}  (r1/r1  +  x\^{}2)  continuous  for  x  \mmember{}  (-\minfty{},  \minfty{})
By
Latex:
(BLemma  `function-is-continuous`  THEN  Auto)
Home
Index