fact: Definition ValAdh (un:nat -> R) (x:R) : Prop := forall (V:R -> Prop) (N:nat), neighbourhood V x -> exists p : nat, (N <= p)%nat /\ V (un p).
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type