Theorems · Theorem · general topology

Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {r : SetRel α α} {s : Set β}
  {f g : β → α},
  (∀ x ∈ s, ContinuousAt f x) →
    (∀ x ∈ s, ContinuousAt g x) → Set.EqOn f g s → r ∈ uniformity α → ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Consider two functions f and g which coincide on a set s and are continuous there. Then there is an open neighborhood of s on which f and g are uniformly close.

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpaceTopologicalSpace