proposition: Lemma ValAdh_un_exists : forall (un:nat -> R) (D:=fun x:R => exists n : nat, x = INR n) (f:= fun x:R => adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)) (x:R), (exists y : R, f x y) -> D x.
proof: Proof. intros; elim H; intros; unfold f in H0; unfold adherence in H0; unfold point_adherent in H0; assert (H1 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). - unfold neighbourhood, disc; exists (mkposreal _ Rlt_0_1); unfold included; trivial. - elim (H0 _ H1); intros; unfold intersection_domain in H2; elim H2; intros; elim H4; intros; apply H6. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type