Step
*
of Lemma
sq_stable__rneq-or
∀x,y:ℝ.  SqStable(x ≠ r0 ∨ y ≠ r0)
BY
{ Extract of Obid: sqs-rneq-or
  not unfolding  find-ge-val bor lt_int absval ifthenelse
  finishing with  (Fold `rneq-zero-or` 0) THEN Auto
  normalizes to:
  
  λx,y,%. rneq-zero-or(x;y) }
Latex:
Latex:
\mforall{}x,y:\mBbbR{}.    SqStable(x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0)
By
Latex:
Extract  of  Obid:  sqs-rneq-or
not  unfolding    find-ge-val  bor  lt\_int  absval  ifthenelse
finishing  with    (Fold  `rneq-zero-or`  0)  THEN  Auto
normalizes  to:
\mlambda{}x,y,\%.  rneq-zero-or(x;y)
Home
Index