English
If f is uniformly continuous on α × α → β and s ⊆ β × β is an entourage, then there exists an entourage u in α such that whenever (a,b) ∈ u, we have (f(a,c), f(b,c)) ∈ s for all c.
Русский
Если f равномерно непрерывна на α × α → β, и s ⊆ β × β является окружением, то существует окружение u в α такое, что если (a,b) ∈ u, то для всех c выполняется (f(a,c), f(b,c)) ∈ s.
LaTeX
$$$\forall s \subseteq (\beta \times \beta)\n (s \in 𝓤(\beta)) \Rightarrow \\exists u \in 𝓤(\alpha), \forall a,b,c, (a,b) \in u \Rightarrow (f(a,c), f(b,c)) \in s$$$
Lean4
theorem mem_uniformity_of_uniformContinuous_invariant [UniformSpace α] [UniformSpace β] {s : Set (β × β)}
{f : α → α → β} (hf : UniformContinuous fun p : α × α => f p.1 p.2) (hs : s ∈ 𝓤 β) :
∃ u ∈ 𝓤 α, ∀ a b c, (a, b) ∈ u → (f a c, f b c) ∈ s :=
by
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf
rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩
exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩
