Theorems · Theorem · general topology

ContinuousMap.uniform_continuity

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [CompactSpace α] [inst_2 : PseudoMetricSpace β]
  (f : C(α, β)) (ε : ℝ), 0 < ε → ∃ δ > 0, ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

Defined in

Mathlib.Topology.ContinuousMap.Compact

Cited by

3 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceCompactSpacePseudoMetricSpace