HolderWith — Mathlib

English

The Hölder condition on an empty set is vacuously satisfied for any constants.

Русский

Условие Хёльдера на пустом множестве выполняется вакуумно для любых констант.

LaTeX

$$$\\operatorname{HolderOnWith} C r f \\emptyset$$$

Lean4

/-- A function `f : X → Y` between two `PseudoEMetricSpace`s 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`. -/
def HolderWith (C r : ℝ≥0) (f : X → Y) : Prop :=
  ∀ x y, edist (f x) (f y) ≤ (C : ℝ≥0∞) * edist x y ^ (r : ℝ)

Похожие утверждения