Theorem MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton

Modification history

2024-08-08 10:31
Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
chore: backports for leanprover/lean4#4814 (part 36) (#15612)
Modified MeasureTheory.GridLines.T_insert_le_T_lmarginal_singletonView on Github →
2024-06-28 22:16
Mathlib/MeasureTheory/Integral/SobolevInequality.lean
feat: prove the Gagliardo-Nirenberg-Sobolev inequality (#14165) …
Added MeasureTheory.GridLines.T_insert_le_T_lmarginal_singletonView on Github →