A Lipschitz function is uniformly continuous

A Lipschitz function is continuous

lipschitz_with K f: the function f is Lipschitz continuous w.r.t. the Lipschitz constant K.

Banach fixed-point theorem, contraction mapping theorem