proposition: Lemma continuity_pt_in_contravariant : forall D E f x, included D E -> continuity_pt_in E f x -> continuity_pt_in D f x.
proof: Proof. intros D E f x inc f_cont Dx ; apply limit1_in_contravariant with E. assumption. apply f_cont, inc ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra