Step
*
of Lemma
rabs-rless-iff
∀x,z:ℝ. (|x| < z
⇐⇒ (-(z) < x) ∧ (x < z))
BY
{ ((UnivCD THENA Auto)
THEN (InstLemma `rabs-difference-bound-iff` [⌜x⌝;⌜r0⌝;⌜z⌝]⋅ THENA Auto)
THEN nRNorm (-1)
THEN Auto) }
Latex:
Latex:
\mforall{}x,z:\mBbbR{}. (|x| < z \mLeftarrow{}{}\mRightarrow{} (-(z) < x) \mwedge{} (x < z))
By
Latex:
((UnivCD THENA Auto)
THEN (InstLemma `rabs-difference-bound-iff` [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{} THENA Auto)
THEN nRNorm (-1)
THEN Auto)
Home
Index