{α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] →
        (f : α → β) → Continuous f → (C : ℝ) → (∀ (x : α), ‖f x‖ ≤ C) → BoundedContinuousFunction α β