Theorems · Theorem · general topology

convex_setOf_holderWith

Deprecated since 2026-07-09Use convex_setOfPred_holderWith instead.

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

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

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace