Theorems · Theorem · general topology

mem_uniformity_of_uniformContinuous_invariant

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : SetRel β β} {f : α → α → β},
  (UniformContinuous fun p => f p.1 p.2) →
    s ∈ uniformity β → ∃ u ∈ uniformity α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace