Theorems · Definition · general topology

HolderWith

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

A function f : X → Y between two PseudoEMetricSpaces is Hölder continuous with constant C : ℝ≥0 and exponent r : ℝ≥0, if edist (f x) (f y) ≤ C * edist x y ^ r for all x y : X.

Defined in

Mathlib.Topology.MetricSpace.Holder

Cited by

47 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace