proposition: Lemma R_interval_open : forall p q, @open RTop [r : R | p < r < q].
proof: Proof. intros p q. replace [r : R | p < r < q] with (Intersection [y : R | y < q] [y : R | y > p]) by (extensionality_ensembles; repeat constructor; lra). eapply (@open_intersection2 RTop). - apply R_lower_beam_open. - apply R_upper_beam_open. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals