proposition: Theorem Rsepare : forall x y:R, x <> y -> exists V : R -> Prop, (exists W : R -> Prop, neighbourhood V x /\ neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)).
proof: Proof. intros x y Hsep; set (D := Rabs (x - y)). cut (0 < D / 2). - intro; exists (disc x (mkposreal _ H)). exists (disc y (mkposreal _ H)); split. + unfold neighbourhood; exists (mkposreal _ H); unfold included; tauto. + split. * unfold neighbourhood; exists (mkposreal _ H); unfold included; tauto. * red; intro; elim H0; intros; unfold intersection_domain in H1; elim H1; intros. cut (D < D). -- intro; elim (Rlt_irrefl _ H4). -- change (Rabs (x - y) < D); apply Rle_lt_trans with (Rabs (x - x0) + Rabs (x0 - y)). ++ replace (x - y) with (x - x0 + (x0 - y)); [ apply Rabs_triang | ring ]. ++ rewrite <-(Rplus_half_diag D); apply Rplus_lt_compat. ** rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2. ** apply H3. - unfold Rdiv; apply Rmult_lt_0_compat. + unfold D; apply Rabs_pos_lt; apply (Rminus_eq_contra _ _ Hsep). + apply Rinv_0_lt_compat; prove_sup0. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type