proposition: Lemma continuity_not_eq_Rball : forall f (D : R -> Prop) x y, D x -> continuity_pt_in D f x -> f x <> y -> exists alp, 0 < alp /\ forall a, D a -> Rball x alp a -> f a <> y.
proof: Proof. intros f D x y Dx f_cont Hneq ; pose (eps := R_dist (f x) y / 2). assert (eps_pos: 0 < eps). unfold eps, Rdiv ; apply Rlt_mult_inv_pos. apply Rabs_pos_lt ; intro Hf ; apply Hneq, Rminus_diag_uniq ; assumption. lra. destruct (f_cont Dx eps eps_pos) as [alp [alp_pos Halp]] ; exists alp ; split. assumption. intros a Da a_in ; apply Rminus_not_eq, Rabs_pos_lt_contravar. transitivity (Rabs (f x - y) - eps). apply Rlt_le_trans with eps ; [assumption | right ; unfold eps, R_dist ; field]. apply Rlt_minus_swap ; apply Rle_lt_trans with (dist R_met (f x - y) (f a - y)) ; [apply Rabs_triang_inv | rewrite R_dist_sym, R_dist_minus_compat]. apply Halp ; split ; [| unfold R_dist] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics