Theorem MeasureTheory.zero_mem_ℒp'

Modification history

2023-06-30 17:15

Mathlib/MeasureTheory/Function/LpSeminorm.lean

feat: define composition of an `AEEqFun` with a (quasi)measure preserving function (#5217)

Modified MeasureTheory.zero_mem_ℒp'View on Github →

2023-05-28 20:07

Mathlib/MeasureTheory/Function/LpSeminorm.lean

feat: port MeasureTheory.Function.LpSeminorm (#4445)

Added MeasureTheory.zero_mem_ℒp'View on Github →