proposition: Lemma ValAdh_un_prop : forall (un:nat -> R) (x:R), ValAdh un x <-> ValAdh_un un x.
proof: Proof. intros; split; intro. - unfold ValAdh in H; unfold ValAdh_un; unfold intersection_family; simpl; intros; elim H0; intros N H1; unfold adherence; unfold point_adherent; intros; elim (H V N H2); intros; exists (un x0); unfold intersection_domain; elim H3; clear H3; intros; split. + assumption. + split. * exists x0; split; [ reflexivity | rewrite H1; apply (le_INR _ _ H3) ]. * exists N; assumption. - unfold ValAdh; intros; unfold ValAdh_un in H; unfold intersection_family in H; simpl in H; assert (H1 : adherence (fun y0:R => (exists p : nat, y0 = un p /\ INR N <= INR p) /\ (exists n : nat, INR N = INR n)) x). + apply H; exists N; reflexivity. + unfold adherence in H1; unfold point_adherent in H1; assert (H2 := H1 _ H0); elim H2; intros; unfold intersection_domain in H3; elim H3; clear H3; intros; elim H4; clear H4; intros; elim H4; clear H4; intros; elim H4; clear H4; intros; exists x1; split. * apply (INR_le _ _ H6). * rewrite H4 in H3; apply H3. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type