Commit 2025-11-26 16:01 f45ec66b

feat: monotonicity of Holderianity (#31561) Prove many results related to the following two:

• If a function is r-Hölder over a bounded space, then it is also s-Hölder when s ≤ r.
• If a function is r-Hölder and t-Hölder, then it is s-Hölder for r ≤ s ≤ t.