田春冰河
2020-02-04 00:00:00 发布
[3/3] 我今天形式化证明了一个勒贝格积分里相当基础的结果：每个 Borel 可测函数在零测度集上都是可积的，进而其积分为零。看似简单的结论，但证明过程相当复杂，因为零测度集可能很大，甚至是不可数的，而这个函数本身可能在相当多的点上取值正无穷或负无穷，证明几乎用到了所有更底层的基础定理。