Theorems · Definition · general topology

UniformContinuous

{α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → (α → β) → Prop

A function f : α → β is uniformly continuous if (f x, f y) tends to the diagonal as (x, y) tends to the diagonal. In other words, if x is sufficiently close to y, then f x is close to f y no matter where x and y are located in α.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

410 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 80 definitions · uses propext, Quot.sound

Assumes

UniformSpaceUniformSpace