fact: Definition locally_2d (P : R -> R -> Prop) x y := exists delta : posreal, forall u v, Rabs (u - x) < delta -> Rabs (v - y) < delta -> P u v.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub