Theorem MeasureTheory.indicatorConstLp_coeFn_nmem

Modification history

2025-05-25 12:30
Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted MeasureTheory.indicatorConstLp_coeFn_nmemView on Github →
2025-04-01 07:44
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
chore: split `MeasureTheory.Function.LpSpace.Basic` (#23508) …
Modified MeasureTheory.indicatorConstLp_coeFn_nmemView on Github →
2023-05-29 08:45
Mathlib/MeasureTheory/Function/LpSpace.lean
feat: port MeasureTheory.Function.LpSpace (#4341)
Added MeasureTheory.indicatorConstLp_coeFn_nmemView on Github →