proposition: Lemma continuous_on_ext : forall (D : T -> Prop) (f g : T -> U), (forall x, D x -> f x = g x) -> continuous_on D f -> continuous_on D g.
proof: Proof. intros D f g H Cf x Dx. apply filterlim_within_ext with (1 := H). rewrite <- H with (1 := Dx). now apply Cf. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq