Theorems · Theorem · general topology

MemHolder.of_le

∀ {Y : Type u_2} [inst : PseudoEMetricSpace Y] {r : NNReal} {X : Type u_3} [inst_1 : PseudoMetricSpace X]
  [hX : BoundedSpace X] {f : X → Y} {s : NNReal}, MemHolder r f → s ≤ r → MemHolder s f

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

Defined in

Mathlib.Topology.MetricSpace.HolderNorm

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoMetricSpaceBoundedSpace