theorem bounded_icc {r_c : ℝ} : Bornology.IsBounded {r : ℝ | 0 ≤ r ∧ r ≤ r_c}

theorem subset_bounded_01 : Bornology.IsBounded (Set.Icc 0 1)

theorem subset_bounded_X {X : Set ℝ} (hX : X ⊆ Set.Icc 0 1) : Bornology.IsBounded X

theorem subset_bounded_A {X A : Set ℝ} (hX : X ⊆ Set.Icc 0 1) (hA : A ⊆ X) : Bornology.IsBounded A

theorem compact_A {A X : Set ℝ} (hX : X ⊆ Set.Icc 0 1) (hA : A ⊆ X) (hClosed : IsClosed A) : IsCompact A

theorem finite_subcover_A {I : Type u_1} {A X : Set ℝ} (hX : X ⊆ Set.Icc 0 1) (hA : A ⊆ X) (hClosed : IsClosed A) (U : I → Set ℝ) (hOpen : ∀ (i : I), IsOpen (U i)) (hCover : A ⊆ ⋃ (i : I), U i) : ∃ (J : Finset I), A ⊆ ⋃ i ∈ J, U i

instance instProperSpaceReal_marginis : ProperSpace ℝ