proposition: Lemma continuous_at_iff_continuity_pt {f : R -> R} {x : R} : @continuous_at RTop RTop f x <-> continuity_pt f x.
proof: Proof. split. - intros H eps H0. assert (neighbourhood (inverse_image f [r : R | Rabs (r - f x) < eps]) x) as H1. { apply RTop_neighborhood_is_neighbourhood, H, open_neighborhood_is_neighborhood. split. - replace [r : R | Rabs (r - f x) < eps] with [r : R | f x - eps < r < f x + eps] by (extensionality_ensembles; constructor; apply Rabs_def1 + apply Rabs_def2 in H1; lra). apply R_interval_open. - constructor. apply Rabs_def1; lra. } destruct H1 as [[alp H1] H2]. exists alp. split; trivial. intros x0 [? H3]. now destruct (H2 _ H3) as [[?]]. - intros H U HU. apply RTop_neighborhood_is_neighbourhood. pose HU as H0. apply RTop_neighborhood_is_neighbourhood in H0. destruct H0 as [[eps H0] H1], (H eps H0) as [alp [H2 H3]]. exists (mkposreal alp H2). intros x' H'. constructor. destruct (Req_dec x x'). + subst. destruct HU as [V [[H4 H5] H6]]. now apply H6. + now apply H1, H3. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)