Theorems · Definition · general topology

ContinuousMap.modulus

{α : Type u_1} →
  {β : Type u_2} →
    [inst : PseudoMetricSpace α] → [CompactSpace α] → [inst_2 : PseudoMetricSpace β] → C(α, β) → (ε : ℝ) → 0 < ε → ℝ

An arbitrarily chosen modulus of uniform continuity for a given function f and ε > 0.

Defined in

Mathlib.Topology.ContinuousMap.Compact

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceCompactSpacePseudoMetricSpace