Theorem MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub

Modification history

2026-02-09 07:29
Mathlib/MeasureTheory/Function/LpSeminorm/LpNorm.lean
feat: real-valued Lᵖ norm (#23881)
Added MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_subView on Github →