{α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] →
        [inst_2 : Lattice β] → [HasSolidNorm β] → [IsOrderedAddMonoid β] → Max (BoundedContinuousFunction α β)