proposition: Lemma R_closed_interval_compact: forall a b:R, a <= b -> compact (SubspaceTopology ([x:RTop | a <= x <= b])).
proof: Proof. intros a b Hbound. apply net_cluster_point_impl_compact. intros. pose (y := fun i:DS_set I => proj1_sig (x i)). destruct (bounded_real_net_has_cluster_point _ y a b). { intros. unfold y. destruct (x i). now destruct i0. } assert (closed [x:RTop | a <= x <= b]). { replace [x:RTop | a <= x <= b] with (Intersection [ x:RTop | a <= x ] [ x:RTop | x <= b ]) by (extensionality_ensembles; do 2 constructor; lra). apply closed_intersection2. - apply upper_closed_interval_closed. + constructor; red; intros; auto with real. apply Rle_trans with y0; trivial. + intros. destruct (total_order_T x1 y0) as [[|]|]; auto with real. - apply lower_closed_interval_closed. + constructor; red; intros; auto with real. apply Rle_trans with y0; trivial. + intros. destruct (total_order_T x1 y0) as [[|]|]; auto with real. } assert (Ensembles.In [x:RTop | a <= x <= b] x0). { rewrite <- (closure_fixes_closed _ H1). apply net_cluster_point_in_closure with y; trivial. destruct H as [i0]. exists i0. intros. constructor. unfold y. destruct (x j). now destruct i. } exists (exist _ x0 H2). red. intros. rewrite subspace_open_char in H3. destruct H3 as [V []]. subst U. destruct H4. red. intros. assert (Ensembles.In V x0). { assumption. } destruct (H0 V H3 H4 i) as [j []]. exists j. split; trivial. now constructor. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals