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