Mathlib v3 is deprecated. Go to Mathlib v4

Theorem integral_eq_zero_of_forall_integral_inner_eq_zero

Modification history

2023-05-15 16:30
src/measure_theory/function/l2_space.lean
chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019) …
Modified integral_eq_zero_of_forall_integral_inner_eq_zeroView on Github →
2021-07-13 07:09
src/measure_theory/set_integral.lean
feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229)
Added integral_eq_zero_of_forall_integral_inner_eq_zeroView on Github →