Theorems · Theorem · general topology

convex_setOfPred_holderWith

∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (f : X → Y) (C : NNReal),
  Convex NNReal {r | HolderWith C r f}

For fixed f : X → Y and C : ℝ≥0, the set of all parameters r : ℝ≥0 such that f is (C, r)-Hölder is convex.

Defined in

Mathlib.Topology.MetricSpace.Holder

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace