proposition: Lemma R_compact_subset_bounded: forall A:Ensemble RTop, compact (SubspaceTopology A) -> bound A.
proof: Proof. intros. destruct (H (Im Full_set (fun y => inverse_image (subspace_inc _) [ x:RTop | y - 1 < x < y + 1 ]))). - intros U [H0]. subst. apply subspace_inc_continuous, R_interval_open. - extensionality_ensembles; econstructor. + now exists (proj1_sig x). + do 2 constructor. destruct x. simpl. lra. - destruct H0, H1. assert (exists a:R, forall S:Ensemble (SubspaceTopology A), forall b:SubspaceTopology A, Ensembles.In x S -> Ensembles.In S b -> proj1_sig b < a). { clear H2. induction H0. - exists 0. intros. destruct H0. - destruct IHFinite. + cut (Included A0 (Add A0 x)); auto with sets. + assert (Ensembles.In (Add A0 x) x). { right. constructor. } apply H1 in H4. destruct H4. exists (Rmax x0 (x+1)). intros. destruct H6. * specialize (H3 x1 b); intuition. apply Rlt_le_trans with x0; auto. apply Rmax_l. * destruct H6. rewrite H5 in H7. destruct H7. destruct H6. apply Rlt_le_trans with (x+1). ** apply H6. ** apply Rmax_r. } destruct H3 as [a]. exists a. red. intros. assert (Ensembles.In (FamilyUnion x) (exist (fun x:R => Ensembles.In A x) x0 H4)). { rewrite H2. constructor. } inversion H5. pose proof (H3 _ _ H6 H7). simpl in H9. auto with real. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals