Louis Wasserman
Louis Wasserman
(I hadn't actually realized that HoTT explicitly endorsed defining uniform continuity without truncation before now.)
I admit I would feel better about that if `function-with-modulus-of-uniform-continuity-Metric-Space` were not so very long even before we add any words describing a result _about_ such functions.
(I hesitate to add, but also, my background in library development strongly suggests that the thing that is actually useful for the significant majority of use cases should get the...
I'm not positive I understand the idiomatic use of capitalization -- `metric-space` versus `Metric-Space` -- which seems associated with structure, maybe? I tend towards `cont` and `ucont` as abbreviations if...
I'd be happy with that.
Only somewhat relatedly: I seem to be getting by with truncated uniform continuity further than I expected to; this may not be necessary (though abbreviations of `uniformly-continuous-function` might still be...
Closing this for the moment, though maybe we should consider the abbreviation aspect separately.
Reopening; I think I may have found a new place where we need the untruncated modulus. I think it may be that the limit of _modulated_ uniformly continuous functions is...
As I think about it, I think we might already have that case: polynomials with real coefficients will certainly not have an untruncated modulus of uniform continuity over any interval;...
I do suppose that most of the "popular" functions in analysis have power series with rational, not simply real, coefficients, and we may still try to do what we can...