Theorem MeasureTheory.Memℒp.toLp_val

Modification history

2025-02-21 20:26

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

Rename `Mem𝓛p` to `MemLp` (#22164) …

Deleted MeasureTheory.Memℒp.toLp_val View on Github →

2024-07-15 20:56

Mathlib/MeasureTheory/Function/LpSpace.lean

feat(Function/LpSpace): continuity of `indicatorConstLp` in the set (#14489)

Added MeasureTheory.Memℒp.toLp_val View on Github →