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