Step
*
of Lemma
rabs_wf
∀[x:ℝ]. (|x| ∈ ℝ)
BY
{ (RWO "rabs-as-rmax" 0 THEN Auto) }
Latex:
Latex:
\mforall{}[x:\mBbbR{}].  (|x|  \mmember{}  \mBbbR{})
By
Latex:
(RWO  "rabs-as-rmax"  0  THEN  Auto)
Home
Index