Theorems · Theorem · general topology

convex_setOf_holderOnWith

Deprecated since 2026-07-09Use convex_setOfPred_holderOnWith instead.

∀ {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}

Alias of convex_setOfPred_holderOnWith. 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

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace