Theorems · Definition · general topology

UniformContinuousOn

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

A function f : α → β is uniformly continuous on s : Set α if (f x, f y) tends to the diagonal as (x, y) tends to the diagonal while remaining in s ×ˢ s. 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 s.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

47 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Quot.sound

Assumes

UniformSpaceUniformSpace