lp_space): add mem_Lp_indicator_iff_restrict (#9221)

Commit

4 years ago

feat(measure_theory/function/lp_space): add mem_Lp_indicator_iff_restrict (#9221) We have an equivalent lemma for `integrable`. Here it is generalized to `mem_ℒp`.

Author

RemyDegenne

Parents

f2c162c1

mathlib 25e67dd8 - feat(measure_theory/function/lp_space): add mem_Lp_indicator_iff_restrict (#9221)

mathlib
25e67dd8 - feat(measure_theory/function/lp_space): add mem_Lp_indicator_iff_restrict (#9221)