nLab almost function

In measure theory, an almost-everywhere-defined function, or almost function, is a partial function whose domain is a full set. We are usually only interested in measurable almost functions. Typically, we consider almost functions up to the equivalence relation of almost equality, whereby two almost functions are almost equal if their equaliser is also a full set, that is if they are equal almost everywhere.

As we need to know what a full set is, there is no notion of almost function on an arbitrary classical measurable space. However, if the measurable space is equipped with such a notion (as is always the case with a Cheng measurable space or a localisable measurable space), then we have almost functions. Of course, a measure space also has plenty of structure for this. The morphisms between measurable locales also inherently correspond to measurable almost functions (up to almost equality).

It is a commonplace that one really only cares about measurable functions up to almost equality. That one only needs measurable functions to be defined almost everywhere is the same idea. However, in classical mathematics, every almost function may be extended (using excluded middle) to an actual (everywhere-defined) function, and this extension is unique up to almost equality. Accordingly, the notion of almost function is only necessary in constructive mathematics. However, even classically, using them from the start can avoid annoying but trivial technicalities. (For example, one does not need the notion of essentially bounded function; bounded almost functions will do.)

Besides measure theory, the concept applies whenever we have a notion of something being true (in this case, that a partial function is defined) almost everywhere.