proposition: Lemma continuous_continuous_on : forall (D : T -> Prop) (f : T -> U) (x : T), locally x D -> continuous_on D f -> continuous f x.
proof: Proof. intros D f x Dx CD P Pfx. assert (Dx' := locally_singleton _ _ Dx). generalize (filter_and _ _ Dx (CD x Dx' P Pfx)). unfold filtermap, within. apply filter_imp. intros t [H1 H2]. now apply H2. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq