Theorems · Definition · general topology

eHolderNorm

{X : Type u_1} → {Y : Type u_2} → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → NNReal → (X → Y) → ENNReal

The r-Hölder (semi-)norm in ℝ≥0∞ of a function f is the least non-negative real number C for which f is r-Hölder continuous with constant C. This is ∞ if no such non-negative real exists.

Defined in

Mathlib.Topology.MetricSpace.HolderNorm

Cited by

16 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace