Having seen many examples of spaces, operators, and adjoints, we should now see more formal definitions, because abstraction helps push concepts to the limit.