Theorems · Theorem · general topology

convex_setOfPred_holderOnWith

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

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

Defined in

Mathlib.Topology.MetricSpace.Holder

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace