Theorems · Definition · general topology

AntilipschitzWith

{α : Type u_1} → {β : Type u_2} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → NNReal → (α → β) → Prop

We say that f : α → β is AntilipschitzWith K if for any two points x, y we have edist x y ≤ K * edist (f x) (f y). This can also be used as a predicate for bounded below linear operators, see antilipschitzWith_iff_exists_mul_le_norm.

Defined in

Mathlib.Topology.MetricSpace.Antilipschitz

Cited by

132 results in Mathlib

Foundations

Depth 147 from the axioms, rests on 3,160 definitions · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpace