Integration with filters #
by Emanuele Bottazzi, Monroe Eskew
The paper concerns measures over [0,∞].
In Lean this interval is known as the type ENNReal, the extended nonnegative reals.
The number ∞ is represented as ⊤.
Here we explore the arithmetic of this type.