FinMatrix.CoqExt.RExt.RExtApprox


Require Export RExtBase RExtAbs RExtBool.

Approximate of two real numbers

r1 ≈ r2, that means |r1 - r2| <= diff
Definition Rapprox (r1 r2 diff : R) : Prop := |r1 - r2| <= diff.

boolean version of approximate function
Definition Rapproxb (r1 r2 diff : R) : bool := |r1 - r2| <=? diff.