Theorems · Definition · general topology

HolderOnWith

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

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

Defined in

Mathlib.Topology.MetricSpace.Holder

Cited by

44 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace