proposition: Lemma RTop_neighborhood_is_neighbourhood (U : Ensemble R) (r : R) : @neighborhood RTop U r <-> neighbourhood U r.
proof: Proof. split. - intros [H1 [[[F H2] [V x H4 H5]] H6]]. eapply (neighbourhood_P1 V). { intros x' H'. apply H6. econstructor. - exact H4. - exact H'. } apply H2 in H4. clear H2 H6 F H1. induction H4. + exists (RinvN 1). now intros ? ?. + destruct H as [y|y]; destruct H5 as [[H5 H6]]; [ refine (ex_intro _ (mkposreal (y - x) _) _) | refine (ex_intro _ (mkposreal (x - y) _) _) ]; intros ? H; apply Rabs_def2 in H; simpl in H; destruct H; repeat constructor; lra. Unshelve. all: lra. + destruct H5 as [x H2 H3], (IHfinite_intersections H2) as [[p Hp] H4], (IHfinite_intersections0 H3) as [[q Hq] H5], (Rlt_or_le p q); [ exists (mkposreal p Hp) | exists (mkposreal q Hq) ]; intros x' H'; apply Rabs_def2 in H'; simpl in H'; destruct H'; constructor; apply H4 + apply H5; apply Rabs_def1; simpl; try assumption; (try now (eapply Rlt_trans; try exact H7); eapply Rlt_trans; try exact H8); lra. - intros [[p Hp] H]. exists [x : R | r - p < x < r + p]. repeat split; try lra. + apply R_interval_open. + intros y [[H1 H2]]. apply H, Rabs_def1; simpl; lra. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals