# 积分为零 ⟺ 几乎处处为零　`prop.integral-zero-iff`
命题：$\int f = 0 \iff f = 0 \text{a.e.}$
layer 17 · 命题 · 积分 · 分析学
[在星图里打开](../#n=prop.integral-zero-iff)　·　[节点索引](../index.md)

设 $f \in L^+$。则

$$\int f d\mu = 0 \iff f = 0 \mu-\text{a.e.}$$

## 为什么成立（入边，证明在 proofs/）
- [`def.null-set`](../nodes/def.null-set.md) 零集与完备：用到了定义 零集与完备　[proofs/def-link.nullset-zeromeasure.md](../proofs/def-link.nullset-zeromeasure.md)
- [`def.ae`](../nodes/def.ae.md) 几乎处处：用到了定义 几乎处处　[proofs/def-link.ae-integral-zero.md](../proofs/def-link.ae-integral-zero.md)

## 它能推出什么 / 谁在用它
- …另有出边，续页见 [nodes/prop.integral-zero-iff.2.md](./prop.integral-zero-iff.2.md)

refs: Folland, Real Analysis, Prop. 2.16

> 说明见 `notes/prop.integral-zero-iff.md`

引用：`prop.integral-zero-iff`（内容 v0.9.0）· 条款见 [LICENSE.txt](../LICENSE.txt)