Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-01-03 16:58
ae2c8572
View on Github →
feat(measure_theory/lp_space): add triangle inequality for the Lp seminorm (
#5594
)
Estimated changes
Modified
src/measure_theory/lp_space.lean
added
theorem
ℒp_space.snorm_add_le