proposition: Lemma continuous_on_forall : forall (D : T -> Prop) (f : T -> U), (forall x, D x -> continuous f x) -> continuous_on D f.
proof: Proof. intros D f H x Dx P Pfx. generalize (H x Dx P Pfx). unfold filtermap, within. now apply filter_imp. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq