Theorems · Theorem · general topology

HolderOnWith.exists_holderOnWith_of_le

∀ {Y : Type u_2} [inst : PseudoEMetricSpace Y] {r : NNReal} {X : Type u_3} [inst_1 : PseudoMetricSpace X] {f : X → Y}
  {s : NNReal} {A : Set X}, (∃ C, HolderOnWith C r f A) → s ≤ r → Bornology.IsBounded A → ∃ C, HolderOnWith C s f A

If a function is r-Hölder over a bounded set, then it is also s-Hölder over this set when s ≤ r. See HolderOnWith.exists_holderOnWith_of_le' for the version in a pseudoemetric space.

Defined in

Mathlib.Topology.MetricSpace.HolderNorm

Cited by

0 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoMetricSpace