BoundedSpace <-> CompactSpace

Stream: mathlib4

[Alex Meiburg]

Should any / all of the four following theorems be instances in Mathlib?

import Mathlib

section r0space

variable {X : Type*} [TopologicalSpace X] [R0Space X]

instance R0Space.boundedSpace_of_compactSpace [CompactSpace X] : @BoundedSpace X (Bornology.relativelyCompact X) := by
  let := Bornology.relativelyCompact X
  constructor
  rw [Bornology.relativelyCompact.isBounded_iff, IsClosed.closure_eq (isClosed_univ)]
  exact CompactSpace.isCompact_univ

instance R0Space.compactSpace_of_boundedSpace [@BoundedSpace X (Bornology.relativelyCompact X)] : CompactSpace X := by
  let := Bornology.relativelyCompact X
  constructor
  rw [← IsClosed.closure_eq (isClosed_univ), ← Bornology.relativelyCompact.isBounded_iff]
  exact BoundedSpace.bounded_univ

end r0space

section pseudometricspace

variable {X : Type*} [PseudoMetricSpace X]

instance PseudoMetricSpace.boundedSpace_of_compactSpace [CompactSpace X] : BoundedSpace X :=
  ⟨CompactSpace.isCompact_univ.isBounded⟩

instance PseudoMetricSpace.compactSpace_of_boundedSpace [ProperSpace X] [BoundedSpace X] : CompactSpace X :=
  ⟨IsClosed.closure_eq (@isClosed_univ X _) ▸ BoundedSpace.bounded_univ.isCompact_closure⟩

end pseudometricspace

[Alex Meiburg]

Currently there's nothing under

#loogle BoundedSpace, CompactSpace